Lemma isplushrelnatlth : @isbinophrel nataddabmonoid natlth. Proof. split. - intros a b c. apply (natgthandplusl b a c). - intros a b c. apply (natgthandplusr b a c). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.NegativePropositions.