proposition: Theorem add_sub_assoc : forall n m p, p <= m -> n + (m - p) == (n + m) - p.
proof: Proof. intros n m p; induct p. - intro; now do 2 rewrite sub_0_r. - intros p IH H. do 2 rewrite sub_succ_r. rewrite <- IH by (apply lt_le_incl; now apply le_succ_l). rewrite add_pred_r by (apply sub_gt; now apply le_succ_l). reflexivity. Qed.
imports: NMulOrder