proposition: Theorem add_sub_eq_l : forall n m p, m + p == n -> n - m == p.
proof: Proof. intros n m p H. symmetry. assert (H1 : m + p - m == n - m) by now rewrite H. rewrite add_comm in H1. now rewrite add_sub in H1. Qed.
imports: NMulOrder