Lemma hzqrandcarryineq ( a : fpscommring hz ) ( n : nat ) : hzleh 0 ( carry a n ) × hzlth ( carry a n ) ( nattohz ( hzabsval m ) ). Proof. intros. split. - unfold carry. apply ( pr2 ( pr1 ( divalgorithm ( precarry a n ) m is ) ) ). - unfold carry. apply ( pr2 ( pr1 ( divalgorithm ( precarry a n ) m is ) ) ). Defined.
Require Import UniMath.PAdics.lemmas. Require Import UniMath.PAdics.fps. Require Import UniMath.PAdics.frac. Require Import UniMath.PAdics.z_mod_p. Require Import UniMath.NumberSystems.Integers.