Lemma isinvplushrelnatlth : @isinvbinophrel nataddabmonoid natlth. Proof. split. - intros a b c. apply (natgthandpluslinv b a c). - intros a b c. apply (natgthandplusrinv b a c). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.NegativePropositions.