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. simple induction j. intros. cut (i = 0); [ intro | auto with arith ]. apply eq_imp_leEq; apply H0; auto. intro m; intros. elim (le_lt_eq_dec _ _ H2); intro. cut (m <= n); [ intro | auto with arith ]. apply leEq_transitive with (f m H3); auto. apply H1; auto with arith. apply eq_imp_leEq; apply H0; assumption. Qed.
imports: CoRN.algebra.COrdAbs Coq(Lia)