Entries from 2016-08-28 to 1 day
前回の続き。 assert((n>1->n=n+0)->(S n>1->n=n+0)). より assert((n>1->n=n+0)->(S n>1->S n=S n+0)). のほうがエレガントですかね。例1 Lemma l3_2: forall (n:nat), n>1 -> n=n+0. Proof. intros. induction n. reflexivity. (* ここがポイント *) asser…
前回の続き。 assert((n>1->n=n+0)->(S n>1->n=n+0)). より assert((n>1->n=n+0)->(S n>1->S n=S n+0)). のほうがエレガントですかね。例1 Lemma l3_2: forall (n:nat), n>1 -> n=n+0. Proof. intros. induction n. reflexivity. (* ここがポイント *) asser…
