Library Coqtail.Arith.PI

Require Import Arith.
Require Import Eqdep_dec.
Require Import Peano_dec.

Theorem K_nat :
   (x:nat) (P:x = xProp), P (refl_equal x) → p:x = x, P p.
  intros; apply K_dec_set with (p := p).
  apply eq_nat_dec.

Theorem eq_rect_eq_nat :
   (p:nat) (Q:natType) (x:Q p) (h:p=p), x = eq_rect p Q x p h.
  intros; apply K_nat with (p := h); reflexivity.

Scheme le_ind := Induction for le Sort Prop.

Two proofs of n<m are equals

Theorem lt_PI : (n m : nat) (pr1 pr2 : n < m),
  pr1 = pr2.
unfold lt ; intros n m ; induction pr1 using le_ind ; intro pr2.
    replace (le_n (S n)) with
      (eq_rect _ (fun n0S n n0) (le_n (S n)) _ (refl_equal (S n))).
      generalize (refl_equal(S n)).
      pattern (S n) at 2 4 6 10, pr2; case pr2; [intro | intros m l e].
      rewrite <- eq_rect_eq_nat; trivial.
      contradiction (le_Sn_n m); rewrite <- e; assumption.
    replace (le_S (S n) m pr1) with
      (eq_rect _ (fun n0S n n0) (le_S (S n) m pr1) _ (refl_equal (S m))).
      generalize (refl_equal (S m)).
      pattern (S m) at 1 3 4 6, pr2; case pr2; [intro Heq | intros m0 l HeqS].
      contradiction (le_Sn_n m); rewrite Heq; assumption.
      injection HeqS; intro Heq; generalize l HeqS.
      rewrite <- Heq; intros; rewrite <- eq_rect_eq_nat.
      rewrite (IHpr1 l0); reflexivity.