proposition: Lemma toCProp_Zlt : forall x y : Z, (x < y)%Z -> Zlts x y.
proof: Proof. intros x y H. unfold Zlts in |- *. unfold Z.lt in H. auto. Qed.
imports: Coq.Arith.Compare_dec CoRN.logic.CornBasics Coq.ZArith.ZArith Coq.setoid_ring.ZArithRing Coq.Arith.Wf_nat Coq(Lia)