proposition: Lemma mul_S_r : forall a b : nat, a * S b =N= a + a * b.
proof: Proof. apply (nat_rect@{N} (fun a => forall b, _));[|intros a IHa];intros b;simpl_nat. - reflexivity. - simpl_nat. rewrite IHa. rewrite (simple_associativity b a). change (((b + a) + (a * b)).+1 =N= (a + Nat.Core.add b (a * b)).+1). rewrite (commutativity (f:=plus) b a), <-(associativity a b). reflexivity. Qed.
imports: HoTT.Classes.interfaces.abstract_algebra HoTT.Classes.interfaces.naturals HoTT.Classes.interfaces.orders HoTT.Classes.theory.rings HoTT.Classes.orders.semirings HoTT.Classes.theory.apartness