1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21
Goal forall m n, n+n = m+m -> m+m = m+m. Proof. intros. set (k := n+n) in *. cut (n=m). intro. subst n. admit. admit. Qed. Goal forall m n, n+n = m+m -> n+n = m+m. Proof. intros. set (k := n+n). cut (n=m). intro. subst n. admit. admit. Qed.