proposition: Lemma isinvmulthrelnatlth : @isinvbinophrel natmultabmonoid natlth.
proof: Proof. split. - intros a b c r. apply (natlthandmultlinv _ _ _ r). - intros a b c r. apply (natlthandmultrinv _ _ _ r). Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Archimedean UniMath.Algebra.Domains_and_Fields UniMath.Algebra.IteratedBinaryOperations