proposition: Lemma nat_local_mon_imp_mon_le : (forall i : nat, h i <= h (S i)) -> forall i j : nat, i <= j -> h i <= h j.
proof: Proof. intros H i j H0. induction j as [| j Hrecj]. cut (i = 0); [ intro H1 | auto with arith ]. rewrite H1; apply le_n. elim (le_lt_eq_dec _ _ H0); intro H1. cut (h i <= h j); [ intro | apply Hrecj; auto with arith ]. cut (h j <= h (S j)); [ intro | apply H ]. apply Nat.le_trans with (h j); auto. rewrite H1; apply le_n. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)