proposition: Lemma mon_imp_mon'_lt : forall n (f : forall i, i < n -> R), nat_less_n_fun f -> (forall i j Hi Hj, i < j -> f i Hi [<] f j Hj) -> forall i j Hi Hj, i <= j -> f i Hi [<=] f j Hj.
proof: Proof. intros. elim (le_lt_eq_dec _ _ H0); intro. apply less_leEq; auto. apply eq_imp_leEq; auto. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)