proposition: Lemma gcdpositive ( n m : hz ) ( i : hzneq 0 n ) : hzlth 0 ( gcd n m i ).
proof: 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.
imports: UniMath.PAdics.lemmas UniMath.NumberSystems.Integers UniMath.Foundations.Preamble