proposition: Theorem lt_Zdigits : forall x y, (0 <= y)%Z -> (Zdigits x < Zdigits y)%Z -> (x < y)%Z.
proof: Proof. intros x y Hy. cut (y <= x -> Zdigits y <= Zdigits x)%Z. lia. now apply Zdigits_le. Qed.
imports: Coq(Lia ZArith Zquot) Zaux