Lemma isrigmultgtnatgth : isrigmultgt natcommrig natgth. 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.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.NegativePropositions.