proposition: Lemma Zdivides_Zmod0_pos : forall a b : Z, (a mod b)%Z = 0%Z -> Zdivides b a.
proof: Proof. intros a b Hmod. rewrite (Z_div_mod_eq_full a b). rewrite (Zmult_comm b (a / b)); rewrite Hmod; rewrite Zplus_0_r. exists (a / b)%Z. reflexivity. Qed.
imports: CoRN.model.Zmod.ZBasics