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.

Definition mod_nat: forall (k l:nat)(H:(l>0)%Z),nat.

Defined.

Lemma mod_nat_correct: forall (k l:nat)(H:(l>0)%Z),
  (k mod l)%Z = (Z_of_nat (mod_nat k l H)).

Lemma nat_Z_div:forall (a b c r:nat)(b' r':Z),
  a=b*c+r->r<c->((Z_of_nat a)=c*b'+r')%Z->(0<=r'<c)%Z-> ((Z_of_nat r)=r').