Lemma isplushrelnatgeh : @isbinophrel nataddabmonoid natgeh. Proof. split. - intros a b c. apply (natlehandplusl b a c). - intros a b c. apply (natlehandplusr b a c). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.NegativePropositions.