(*
Goal forall x y, S x=S y -> x-y=0.
intros.
case H.
*)

Definition pred x := match x with
  O => O
| S n => n
end.

Lemma S_inj : forall n m, S n=S m -> n=m.
intros.
change (pred (S n) = pred (S m)).
rewrite H.
reflexivity.
Qed.

Goal forall x y, S x=S y -> x-y=0.
intros.

(*
rewrite (S_inj x y).
Focus 2.
*)
injection H.
Show Proof.

intro.
rewrite H0.

clear H H0.
induction y.
simpl.
reflexivity.
simpl.
assumption.
Qed.

(* trivial! *)

Require Import List.

Goal forall (a:nat) l b l', cons a l = cons b l' -> cons b l = cons a l'.
intros.
injection H.
Show Proof.

intros.
subst.
reflexivity.
Qed.