Lemma commonhzdivsignswap ( k n m : hz ) ( p : iscommonhzdiv k n m ) : iscommonhzdiv ( - k ) n m . Proof. intros. destruct p as [ p0 p1 ]. split. - use (hinhuniv _ p0). intro t. intros P s. apply s. destruct t as [ l f ]. unfold hzdiv0 in f. split with ( - l ). unfold hzdiv0. change ( k * l ) with ( k * l )%ring in f. rewrite <- ringmultminusminus in f. assumption. - use (hinhuniv _ p1). intro t. destruct t as [ l f ]. unfold hzdiv0 in f. intros P s. apply s. split with ( - l ). unfold hzdiv0. change ( k * l ) with ( k * l )%ring in f. rewrite <- ringmultminusminus in f. assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.