Lemma hzdivlinearcombleft ( a b c d : hz ) ( f : a = b + c ) ( x : hzdiv d a ) ( y : hzdiv d b ) : hzdiv d c. Proof. intros P s. use (hinhuniv _ x). intro x'. use (hinhuniv _ y). intro y'. apply s. destruct x' as [ k g ]. destruct y' as [ l h ]. unfold hzdiv0 in *. split with ( k + - l ). rewrite hzldistr. rewrite g. rewrite ( ringrmultminus hz ). change ( ( a + ( - ( d * l ) ) )%hz = c ). rewrite h. apply ( hzplusrcan _ _ b ). rewrite hzplusassoc. rewrite hzlminus. rewrite hzplusr0. rewrite hzpluscomm. assumption. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.