a b : (S a) * b =N= b + a * b := idpath. Local Instance mul_1_l : LeftIdentity@{N N} (mult : Mult nat) (one : One nat) := add_0_r. Local Instance mul_0_r : RightAbsorb@{N N} (mult : Mult nat) (zero : Zero nat). Proof. intros a; induction a as [| a IHa]. - reflexivity. - change (a * 0 = 0). exact IHa. Qed.
Require Import