proposition: Lemma pred_lt : forall m n : nat, m < pred n -> S m < n.
proof: Proof. intros; apply Nat.le_lt_trans with (pred n); auto with arith. apply Nat.lt_pred_l; apply Nat.neq_0_lt_0. apply Nat.le_lt_trans with m. auto with arith. 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)