proposition: Theorem le_uniqueness_proof : forall (n m : nat) (p q : le n m), p = q.
proof: Proof. induction p using le_ind'; intro q. replace (le_n n) with (eq_rect _ (fun n0 => le n n0) (le_n n) _ (refl_equal n)). 2:reflexivity. generalize (refl_equal n). pattern n at 2 4 6 10, q; case q; [intro | intros m l e]. rewrite <- (eq_rect_eq_dec eq_nat_dec); eauto. contradiction (le_Sn_n m); rewrite <- e; assumption. replace (le_S n m p) with (eq_rect _ (fun n0 => le n n0) (le_S n m p) _ (refl_equal (S m))). 2:reflexivity. generalize (refl_equal (S m)). pattern (S m) at 1 3 4 6, q; case q; [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_dec eq_nat_dec). rewrite (IHp l0); reflexivity. Qed.
imports: Fiat.Common.Coq__8_4__8_5__Compat Bedrock.Word Coq.ZArith.ZArith Coq.NArith.NArith Coq.Arith.Arith Coq.Numbers.Natural.Peano.NPeano Coq.Logic.Eqdep_dec Fiat.Narcissus.Common.Specs