proposition: Lemma Zmod_pos:(forall (k l:nat)(H:(l>0)%Z), (k mod l)%Z=0 or {p:positive|(k mod l)%Z =(Zpos p)}):CProp.
proof: Proof. simpl. intros k l. intro H0. set (H:= (Z_mod_lt k l H0)). elim H. clear H. intros H1 H2. elim (Z_le_lt_eq_dec 0 (k mod l)%Z H1). case (k mod l)%Z. intuition. intros p H. right. exists p. reflexivity. intros p H3. 2:intuition. cut False. intuition. cut (Zneg p < 0)%Z. intuition. unfold Z.lt. intuition. Qed.
imports: CoRN.model.Zmod.ZMod CoRN.logic.CLogic