Lemma hzdivlinearcombright ( a b c d : hz ) ( f : a = b + c ) ( x: hzdiv d b ) ( y : hzdiv d c ) : hzdiv d a. 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. change ( (d * k + d * l)%hz = a ). rewrite g, h, f. apply idpath. Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.NumberSystems.Integers. Require Import UniMath.Foundations.Preamble.