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