proposition: Lemma Zmod0_Zdivides_pos : forall a b : Z, (b > 0)%Z -> Zdivides b a -> (a mod b)%Z = 0%Z.
proof: Proof. intros a b Hb Hdiv. elim Hdiv; intros q Hq. rewrite (Z_div_mod_eq_full a b) in Hq. rewrite <- (Zplus_0_r (q * b)) in Hq. symmetry in |- *. apply (Zdiv_remainder_unique (q * b + 0) b q 0 (a / b) (a mod b)). reflexivity. auto with zarith. rewrite (Zmult_comm (a / b) b); exact Hq. apply Z_mod_lt; auto with zarith. Qed.
imports: CoRN.model.Zmod.ZBasics