これは楽勝。 Lemma l2: forall (n:nat), n=n+0. Proof. intros. induction n. reflexivity. simpl. f_equal. apply IHn. Qed. しかし式をforall (n:nat), n>1 -> n=n+0.にすると、 普通にやると、ゴールがn>1、仮定がS n>1となりうまくいきません。 そこで…