proposition: Lemma hzdivandminus ( a d : hz ) ( p : hzdiv d a ) : hzdiv d ( - a ).
proof: Proof. intros. intros P s. use (hinhuniv _ p). intro k. destruct k as [ k f ]. apply s. split with ( - k ). unfold hzdiv0. unfold hzdiv0 in f. rewrite ( ringrmultminus hz ). apply maponpaths. assumption. Defined.
imports: UniMath.PAdics.lemmas UniMath.NumberSystems.Integers UniMath.Foundations.Preamble