proposition: Lemma isrigmultgtnatgth : isrigmultgt natcommrig natgth.
proof: Proof. intros a. induction a as [|a IHa]. - intros ? ? ? rab rcd. contradicts rab (negnatgth0n b). - intros ? ? ? rab rcd. induction b as [|b IHb]. + simpl. rewrite 2 natplusr0. apply natlthandmultl. * exact tt. * exact rcd. + simpl. set (rer := abmonoidrer nataddabmonoid). unfold op1, op2; simpl. rewrite (rer _ _ _ d). rewrite (rer _ _ _ c). unfold op1, op2; simpl. rewrite (natpluscomm c d). apply (natlthandplusr (a * d + b * c) (a * c + b * d) (d + c)). apply (IHa _ _ _ rab rcd). Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Archimedean UniMath.Algebra.Domains_and_Fields UniMath.Algebra.IteratedBinaryOperations