Lemma hzlthminusequiv ( n m : hz ) : ( hzlth n m -> hzlth 0 ( m - n ) ) × ( hzlth 0 ( m - n ) -> hzlth n m ). Proof. intros. rewrite <- ( hzrminus n ). change ( n - n ) with ( n + - n ). change ( m - n ) with ( m + - n ). split. - intro p. apply hzlthandplusr. assumption. - intro p. rewrite <- ( hzplusr0 n ). rewrite <- ( hzplusr0 m ). rewrite <- ( hzlminus n ). rewrite <- 2! hzplusassoc. apply hzlthandplusr. assumption. Defined.
Require Import UniMath.Foundations.PartA. Require Import UniMath.Foundations.Propositions. Require Import UniMath.Foundations.NaturalNumbers. Require Import UniMath.Algebra.RigsAndRings. Require Import UniMath.Algebra.Domains_and_Fields. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Algebra.Monoids.