proposition: Lemma isplushrelnatgth : @isbinophrel nataddabmonoid natgth.
proof: Proof. split. apply natgthandplusl. apply natgthandplusr. Defined.
imports: UniMath.Foundations.NaturalNumbers UniMath.MoreFoundations.Tactics UniMath.MoreFoundations.NegativePropositions UniMath.Algebra.Archimedean UniMath.Algebra.Domains_and_Fields UniMath.Algebra.IteratedBinaryOperations