proposition: Lemma divide_sub_r : forall n m p, (n | m) -> (n | p) -> (n | m - p).
proof: Proof. intros n m p H H'. rewrite <- add_opp_r. apply divide_add_r; trivial. now apply divide_opp_r. Qed.
imports: ZAxioms ZMulOrder ZSgnAbs NZGcd