Require Import Lt.

Definition f (n:nat) := n*n.

(* assert, generalize, generalize at as *)
Lemma cos: forall n, f n + f n = f n -> n=0.
intro n.
intro.
assert (f n = 0).
revert H.
generalize (f n) as m.
intro.

generalize m at 2 4 as k.
induction m; simpl.
auto.
intros.
injection H.
apply IHm.

clear H.
subst.

destruct n.
reflexivity.

unfold f in H0.
simpl in H0.
discriminate.
Qed.

(* set/pose, assert *)
Lemma cos1: forall n, f n + f n = f n -> n=0.
intro n.
set (m:=f n).
intro.
assert (m=0).
revert H.

generalize m at 2 4 as k.
induction m; simpl.
auto.
intros.
injection H.
apply IHm.

clear H.
subst.

destruct n.
reflexivity.

unfold f in H0.
simpl in H0.
discriminate.
Qed.

(* generalize dependent *)
Lemma cos2: forall n, f n + f n = f n -> n=0.
intros.
assert (H0 : f n = 0).
generalize dependent (f n).
intro m.

generalize m at 2 4 as k.
induction m; simpl.
auto.
intros.
injection H.
apply IHm.

clear H.

destruct n.
reflexivity.

unfold f in H0.
simpl in H0.
discriminate.
Qed.