proposition: Lemma Zmod0_Zdivides : forall a b : Z, b <> 0%Z -> Zdivides b a -> (a mod b)%Z = 0%Z.
proof: Proof. intros a b. case b. tauto. intros p _; apply Zmod0_Zdivides_pos; auto with zarith. intros p _. generalize (Zmod0_Zdivides_pos a (Zpos p)); intro H. fold (- Zpos p)%Z in |- *. intro Hdiv. apply Zmod0_Zopp. intro; discriminate. apply H. auto with zarith. rewrite <- (Z.opp_involutive (Zpos p)). apply Zdivides_opp_elim_lft. assumption. Qed.
imports: CoRN.model.Zmod.ZBasics