proposition: Lemma nat_mon_imp_inj : (forall i j : nat, i < j -> h i < h j) -> forall i j : nat, h i = h j -> i = j.
proof: Proof. intros H i j H0. cut (~ i <> j); [ lia | intro H1 ]. cut (i < j \/ j < i); [ intro H2 | lia ]. inversion_clear H2. cut (h i < h j); [ rewrite H0; apply Nat.lt_irrefl | apply H; assumption ]. cut (h j < h i); [ rewrite H0; apply Nat.lt_irrefl | apply H; assumption ]. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)