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