proposition: Lemma divide_sub_r : forall n m p, (n | m) -> (n | p) -> (n | m - p).
proof: Proof. intros n m p H H'. destruct (le_ge_cases m p) as [LE|LE]. - apply sub_0_le in LE. rewrite LE. apply divide_0_r. - apply divide_add_cancel_r with p; trivial. now rewrite add_comm, sub_add. Qed.
imports: NAxioms NSub NZGcd