2025-01-14 (Tue)
#1 forall {m n : nat} (H : m.+1 = n.+1), f_equal succn (f_equal predn H) = H を証明する
昨日の my_vector_caseS で Hn を noconf_nat_inv Hn noconf_nat に置き換えるのに
noconf_natK という補題を使った。
そのために no con
Hena Hena Nikki
2003|05|06|07|08|09|10|11|12|
2004|01|02|03|04|05|06|07|08|09|10|11|12|
2005|01|02|03|04|05|06|07|08|09|10|11|12|
2006|01|02|03|04|05|06|07|08|09|10|11|12|
2007|01|02|03|04|05|06|07|08
2010年04月20日(火)[同じ日付をまとめて見る]
#1 納品書兼領収書
amazonから届いた箱を開けて内容を確認すると納品書に見覚えのない文字が...納品書の宛て名を確かめるとわしの名ではない文字が...うぅぅ! 梱包ミスか!!と思って中身を確かめるとわし宛ての納品書とそれに従った中身が入っていた。つまりはわし宛てではない納品書がまぎれて梱包されている。
わし的には何ら問題は無いのだけれど