proposition: Lemma lt_10 : forall i m n : nat, 0 < i -> i < pred (m + n) -> pred i < pred m + pred n.
proof: Proof. intros; lia. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)