proposition: Theorem add_sub_swap : forall n m p, p <= n -> n + m - p == n - p + m.
proof: Proof. intros n m p H. rewrite (add_comm n m). rewrite <- add_sub_assoc by assumption. now rewrite (add_comm m (n - p)). Qed.
imports: NMulOrder