proposition: Lemma divide_add_cancel_r : forall n m p, (n | m) -> (n | m + p) -> (n | p).
proof: Proof. intros n m p (q,Hq) (r,Hr). exists (r-q). rewrite mul_sub_distr_r, <- Hq, <- Hr. now rewrite add_comm, add_sub. Qed.
imports: NAxioms NSub NZGcd