proposition: Lemma hzlthminus ( n m k : hz ) ( p : hzlth n k ) ( q : hzlth m k ) ( q' : hzleh 0 m ) : hzlth ( n - m ) k.
proof: 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.
imports: UniMath.Tactics.EnsureStructuredProofs UniMath.Foundations.PartA UniMath.Foundations.Propositions UniMath.Foundations.NaturalNumbers UniMath.Algebra.RigsAndRings UniMath.Algebra.Domains_and_Fields UniMath.NumberSystems.Integers UniMath.Algebra.Monoids