(*
Goal 0<>1.
unfold not.
intro.
*)

Definition P (n:nat) := 
  match n with 
    O => True
  | S _ => False
  end.

Print False.
Print True.

Goal 0<>1.
unfold not.
intro.
change (P 1).
rewrite <- H.
simpl.
split.
Show Proof.
Qed.

Goal 0<>1.
intro.
discriminate H.
Show Proof.
Qed.

Goal true = false -> 0=1.
discriminate 1.
Show Proof.