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