proposition: Lemma hzlthminusswap ( n m : hz ) ( p : hzlth n m ) : hzlth ( - m ) (- n ).
proof: Proof. intros. rewrite <- ( hzplusl0 ( - m ) ). rewrite <- ( hzrminus n ). change ( hzlth ( n + - n + - m ) ( - n ) ). rewrite hzplusassoc. rewrite ( hzpluscomm ( -n ) ). rewrite <- hzplusassoc. assert ( - n = 0 + - n ) as f. { apply pathsinv0. apply hzplusl0. } assert ( hzlth ( n + - m + - n ) ( 0 + - n ) ) as q. { apply hzlthandplusr. rewrite <- ( hzrminus m ). change ( m - m ) with ( m + - m ). apply hzlthandplusr. assumption. } rewrite <- f in q. 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