proposition: Lemma Zdivides_abs_intro_rht : forall a b : Z, Zdivides a (Z.abs b) -> Zdivides a b.
proof: Proof. intros a b. case b; simpl in |- *; auto. intros p; apply (Zdivides_opp_intro_rht a (Zneg p)). Qed.
imports: CoRN.model.Zmod.ZBasics