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