proposition: Lemma nat_local_mon_imp_mon : (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]. exfalso; lia. cut (i <= j); [ intro H1 | auto with arith ]. elim (le_lt_eq_dec _ _ H1); intro H2. cut (h i < h j); [ intro | apply Hrecj; assumption ]. cut (h j < h (S j)); [ intro | apply H ]. apply Nat.lt_trans with (h j); auto. rewrite H2; apply H. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)