proposition: Theorem sub_add_distr : forall n m p, n - (m + p) == (n - m) - p.
proof: Proof. intros n m p; induct p. - rewrite add_0_r; now rewrite sub_0_r. - intros p IH. rewrite add_succ_r; do 2 rewrite sub_succ_r. now rewrite IH. Qed.
imports: NMulOrder