proposition: Theorem mul_sub_distr_r : ∀ n m p, p ≠ ∞ → (n - m) * p = n * p - m * p.
proof: Proof. intros n m p Hp. destruct p as [p| ]; [ simpl | negation Hp ]. destruct m as [m| ]; [ simpl | reflexivity ]. destruct n as [n| ]; [ simpl | reflexivity ]. rewrite Nat.mul_sub_distr_r; reflexivity. Qed.
imports: Utf8 Compare_dec NPeano Misc