Lemma hzlthminus ( n m k : hz ) ( p : hzlth n k ) ( q : hzlth m k ) ( q' : hzleh 0 m ) : hzlth ( n - m ) k. Proof. intros. destruct ( hzlehchoice 0 m q' ) as [ l | r ]. - apply ( istranshzlth _ n _ ). + assert ( hzlth ( n - m ) ( n + 0 ) ) as i0. { rewrite <- ( hzrminus m ). change ( m - m ) with ( m + - m ). rewrite <- hzplusassoc. apply hzlthandplusr. assert ( hzlth ( n + 0 ) ( n + m ) ) as i00. { apply hzlthandplusl. assumption. } rewrite hzplusr0 in i00. assumption. } rewrite hzplusr0 in i0. assumption. + assumption. - rewrite <- r. change ( n - 0 ) with ( n + - 0 ). rewrite hzminuszero. rewrite ( hzplusr0 n ). 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.