proposition: Lemma hzqrandcarryineq ( a : fpscommring hz ) ( n : nat ) : hzleh 0 ( carry a n ) × hzlth ( carry a n ) ( nattohz ( hzabsval m ) ).
proof: 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.
imports: UniMath.PAdics.lemmas UniMath.PAdics.fps UniMath.PAdics.frac UniMath.PAdics.z_mod_p UniMath.NumberSystems.Integers