Lemma gcdpositive ( n m : hz ) ( i : hzneq 0 n ) : hzlth 0 ( gcd n m i ). Proof. intros. destruct ( hzneqchoice 0 ( gcd n m i ) ( gcdneq0 n m i ) ) as [ left | right ]. - apply fromempty. assert ( hzleh ( - ( gcd n m i ) ) ( gcd n m i ) ) as i0. { apply ( gcdisgreatest n m i ). apply commonhzdivsignswap. exact ( gcdiscommondiv n m i ). } apply ( isirreflhzlth 0 ). apply ( istranshzlth _ ( - ( gcd n m i ) ) _ ). + apply hzlth0andminus. assumption. + apply ( hzlehlthtrans _ ( gcd n m i ) _ ); assumption. - assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.