proposition: 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').
proof: Proof. intros a b c0 r b' r' H H1 H2 H3. cut (c0>0)%Z. intro H5. 2:intuition. set (H4:=(Z_div_mod_eq_full (Z_of_nat a) (Z_of_nat c0))). cut ((Z_of_nat a mod (Z_of_nat c0))%Z = r'). intro H6. rewrite<- H6. cut ((Z_of_nat a mod (Z_of_nat c0))%Z= (Z_of_nat r)). intro H7. rewrite<- H7. reflexivity. rewrite H. set (H8:= (Zmod_cancel_multiple c0 r b H5)). set (H9:= (inj_mult b c0)). set (H10:= (inj_plus (b*c0) r)). rewrite H10. rewrite H9. rewrite H8. apply Zmod_small. intuition. intuition. rewrite H2. replace (Z_of_nat c0 * b' + r')%Z with ( b'*Z_of_nat c0 + r')%Z. 2:intuition. set (H8:= (Zmod_cancel_multiple c0 r' b' H5)). rewrite H8. apply Zmod_small; intuition. Qed.
imports: CoRN.model.Zmod.ZMod CoRN.logic.CLogic