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