proposition: Lemma commonhzdivsignswap ( k n m : hz ) ( p : iscommonhzdiv k n m ) : iscommonhzdiv ( - k ) n m .
proof: 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.
imports: UniMath.PAdics.lemmas UniMath.NumberSystems.Integers UniMath.Foundations.Preamble