proposition: Theorem mul_sub_distr_r : forall n m p, (n - m) * p == n * p - m * p.
proof: Proof. intros n m p; induct n. - now rewrite sub_0_l, mul_0_l, sub_0_l. - intros n IH. destruct (le_gt_cases m n) as [H | H]. + rewrite sub_succ_l by assumption. do 2 rewrite mul_succ_l. rewrite (add_comm ((n - m) * p) p), (add_comm (n * p) p). rewrite <- (add_sub_assoc p (n * p) (m * p)) by now apply mul_le_mono_r. now apply add_cancel_l. + assert (H1 : S n <= m) by now apply le_succ_l. setoid_replace (S n - m) with 0 by now apply sub_0_le. setoid_replace ((S n * p) - m * p) with 0 by (apply sub_0_le; now apply mul_le_mono_r). apply mul_0_l. Qed.
imports: NMulOrder