proposition: Lemma Zdivides_spec : forall (a b : Z), Zdivides a b -> (a * (b / a) = b)%Z.
proof: Proof. intros a b Hdiv. case (Z.eq_dec a 0). intro H; rewrite H; simpl. symmetry; apply Zdivides_zero_lft; rewrite <- H; assumption. intro Hap. rewrite <- Z_div_exact_full_2. reflexivity. assumption. case (Z.eq_dec a 0). now intro H; rewrite H in Hap. intro H; clear H. apply Zmod0_Zdivides; assumption. Qed.
imports: CRings Zring