proposition: Lemma lt_8 : forall m n : nat, m < pred n -> m < n.
proof: Proof. intros; apply Nat.lt_le_trans with (pred n); auto with arith. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)