forall (m n : binnat), (Succ m) * n = n + (m * n). Proof. induction m. - intros n. change (bzero + n = n + bzero). apply commutativity. - intros n. simpl. change (double2 m * n) with ((m * n) + (m * n) + n + n). apply commutativity. - intros n. simpl. change (double1 (Succ m) * n) with ((Succ m) * n + (Succ m) * n + n). rewrite IHm. rewrite (commutativity n (double2 m * n)). rewrite (commutativity n (m * n)). rewrite <- (associativity (m * n) n (m * n + n)). rewrite (commutativity n (m * n + n)). rewrite (associativity (m * n) _ _). rewrite (associativity (m * n) (m * n) n). done. Qed.
Require Import Require Import Require Import