proposition: Theorem mul_pred_r : forall n m, n * (P m) == n * m - n.
proof: Proof. intros n m; cases m. - now rewrite pred_0, mul_0_r, sub_0_l. - intro m; rewrite pred_succ, mul_succ_r, <- add_sub_assoc. + now rewrite sub_diag, add_0_r. + now apply eq_le_incl. Qed.
imports: NMulOrder