proposition: Lemma lt_pred' : forall m n : nat, 0 < m -> m < n -> pred m < pred n.
proof: Proof. intros m n H H0; red in |- *. destruct n. inversion H0. rewrite (Nat.lt_succ_pred 0 m); auto. simpl in |- *. 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)