proposition: Lemma divide_opp_l : forall n m, (-n | m) <-> (n | m).
proof: Proof. intros n m. split; intros (p,Hp); exists (-p); rewrite Hp. - now rewrite mul_opp_l, mul_opp_r. - now rewrite mul_opp_opp. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZGcd