Lemma ispartinvmulthrelnatleh : @ispartinvbinophrel natmultabmonoid (λ x, x ≠ 0) natleh. Proof. split. - intros a b c s r. apply (natlehandmultlinv _ _ _ s r). - intros a b c s r. apply (natlehandmultrinv _ _ _ s r). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.NegativePropositions.