Goal 0=1 -> 0=5.
intro.
try tauto.
repeat rewrite <- H.
progress auto.
Qed.

Ltac tak n := intro n; elim n.

Goal forall m:nat, m=m.
tak m.
auto.
auto.
Qed.


Ltac uprosc H := 
  match type of H with 
  | O=(S _) => idtac "pierwszy"; discriminate H 
  | (S ?n)=(S ?m) => idtac "drugi"; injection H; clear H; intro H
  end.

Goal forall m, 1=(S m) -> m=1 -> 4>6.
intros.
uprosc H.
rewrite H0 in H.
uprosc H.
Qed.


Ltac inj H := 
  match type of H with 
  | (S ?n)=(S ?m) => constr:(n=m)
  end.

Ltac cutinj H W :=
  let t:=inj H in 
  let n:=fresh W in
  cut t; [intro n | ].

Goal forall m, 1=(S m) -> 4>6.
intros.
cutinj H m.
Admitted.


Ltac cutinj2 H W :=
  let t:=inj H in 
  let n:=fresh W in
  let m:=3 in
  let k:=m in
  let cw w := do w cut t in
  cw k; [intro n; intro z | ..].

Goal forall m, 1=(S m) -> 4>6.
intros.
cutinj2 H B.
Admitted.