Lemma isinvplushrelnatgeh : @isinvbinophrel nataddabmonoid natgeh. Proof. split. - intros a b c. apply (natlehandpluslinv b a c). - intros a b c. apply (natlehandplusrinv b a c). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.NegativePropositions.