Induction.v

二進数のnormalizeに関して、normalizeした二進数が必ずnormalizeする前のものより短くなることを証明してみた。

証明することは出来たが、命題に対する帰納法ってやつをあんまり理解していないことが分かった。(最初、n <= m -> S n <= S mを証明するために、nに関する帰納法でやってしまって泥沼に嵌った。)

まあでも以前と違って、何を理解していないかが明確に分かってきた気がする。

鍵は木だと思う。