Lemma inject_nat : forall n m :nat, S n = S m -> n = m.
Proof.
intros n m Heq.
inversion_clear Heq.
reflexivity.
Qed.

Print le.

(* 
Inductive le (n : nat) : nat -> Prop :=
    le_n : n <= n 
  | le_S : forall m : nat, n <= m -> n <= S m
*)

Check le_ind.
(*
le_ind
     : forall (n : nat) (P : nat -> Prop),
       P n ->
       (forall m : nat, n <= m -> P m -> P (S m)) ->
       forall n0 : nat, n <= n0 -> P n0 
*)

Lemma basic1 :forall n : nat, le n 0 -> n = 0.
Proof.
induction n.
auto.
intro H.
(* And now what?? *)
inversion H.
(* inversion analyses the possible cases for H; 
   there is none (!), because the types of le_n and le_S don't match on the type of H,
   so the type "S n <= 0" is empty, so we can conclude everything, and we have a proof of S n = 0 *)
Qed.

(* Different proof of the same lemma 
   There is no need to do an induction on n *)
Lemma basic2 :forall n : nat, le n 0 -> n = 0.
Proof.
intros n H.
inversion H.
(* only le_n can be a proof of n <= 0 *)
(* NB inversion_clear H removes all superfluous hypotheses 
   from the context *)
auto.
Qed.

(* Here you see what hypotheses inversion creates *)
Lemma explain_inversion : forall R : nat -> nat -> Prop, forall n m : nat, le n m -> R n m.
Proof.
intros R n m H.
inversion H.
(* inversion has created two goals, one for each case of the constructor of <= 
   To see the second goal: *)
Show 2.
Abort.

Inductive even : nat -> Prop :=
| even_O : even O
| even_S_S : forall n, even n -> even (S (S n)).

Print even.

Lemma base1_even : ~ even 1.
intro H.
inversion H.
Qed.

Lemma base2_even : forall n, ~ even n -> ~even (S (S n)).
(* Prove using inversion_clear *)
Admitted.

Inductive odd : nat -> Prop :=
| odd_1 : odd 1
| odd_S_S : forall n, odd n -> odd (S (S n)).

Lemma base1_odd :  ~ odd 0.
Admitted.

Lemma base2_odd : forall n, ~ odd n -> ~odd (S (S n)).
(* Prove using inversion_clear *)
Admitted.

Print option.
Lemma option_eq : forall x y : nat, Some x = Some y -> x =y.
Proof.
intros x y H.
inversion H.
(* This derives x=y from Some x = Some y, 
   which holds because Some is a constructor *)
reflexivity.
Qed.

Lemma option_eq1 : forall x : nat, Some x <> None.
intro x.
intro H.
inversion H.
Qed.