Lemma hzlthminusswap ( n m : hz ) ( p : hzlth n m ) : hzlth ( - m ) (- n ). 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.
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.