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