proposition: Lemma mon_imp_inj_lt : forall n (f : forall i, i < n -> R), (forall i j Hi Hj, i < j -> f i Hi [<] f j Hj) -> forall i j Hi Hj, f i Hi [=] f j Hj -> i = j.
proof: Proof. intros. cut (~ i <> j); intro. clear X H Hj Hi; lia. cut (i < j \/ j < i); [ intro | apply not_eq; auto ]. inversion_clear H1; (exfalso; cut (f i Hi [#] f j Hj); [ apply eq_imp_not_ap; assumption | idtac ]). apply less_imp_ap; auto. apply Greater_imp_ap; auto. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)