proposition: Theorem Zdigits_le : forall x y, (0 <= x)%Z -> (x <= y)%Z -> (Zdigits x <= Zdigits y)%Z.
proof: Proof. intros x y Zx Hxy. assert (Hx := Zdigits_correct x). assert (Hy := Zdigits_correct y). apply (Zpower_lt_Zpower beta). lia. Qed.
imports: Coq(Lia ZArith Zquot) Zaux