Lemma isinvrigmultgtnatgth : isinvrigmultgt natcommrig natgth. Proof. set (rer := abmonoidrer nataddabmonoid). simpl in rer. apply isinvrigmultgtif. intros a b c d. generalize a b c. clear a b c. induction d as [ | d IHd ]. - intros a b c g gab. change (pr1 ((a * c + b * 0) > (a * 0 + b * c))) in g. destruct c as [ | c ]. + rewrite (natmultn0 _) in g. destruct (isirreflnatgth _ g). + apply natgthsn0. - intros a b c g gab. destruct c as [ | c ]. + change (pr1 ((a * 0 + b * S d) > (a * S d + b * 0))) in g. rewrite (natmultn0 _) in g. rewrite (natmultn0 _) in g. rewrite (natplusl0 _) in g. rewrite (natplusr0 _) in g. set (g' := natgthandmultrinv _ _ _ g). destruct (isasymmnatgth _ _ gab g'). + change (pr1 (natgth (a * S c + b * S d) (a * S d + b * S c))) in g. rewrite (multnsm _ _) in g. rewrite (multnsm _ _) in g. rewrite (multnsm _ _) in g. rewrite (multnsm _ _) in g. rewrite (rer _ (a * c) _ _) in g. rewrite (rer _ (a * d) _ _) in g. set (g' := natgthandpluslinv _ _ (a + b) g). apply (IHd a b c g' gab). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.NegativePropositions.