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