proposition: Lemma ispartinvmulthrelnatleh : @ispartinvbinophrel natmultabmonoid (λ x, x ≠ 0) natleh.
proof: Proof. split. - intros a b c s r. apply (natlehandmultlinv _ _ _ s r). - intros a b c s r. apply (natlehandmultrinv _ _ _ s r). Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Archimedean UniMath.Algebra.Domains_and_Fields UniMath.Algebra.IteratedBinaryOperations