proposition: Lemma nat_mon_imp_mon' : (forall i j : nat, i < j -> h i < h j) -> forall i j : nat, i <= j -> h i <= h j.
proof: Proof. intros H i j H0. elim (le_lt_eq_dec _ _ H0); intro H1. apply Nat.lt_le_incl; apply H; assumption. 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)