proposition: Theorem Zdigits_mult_ge : forall x y, (x <> 0)%Z -> (y <> 0)%Z -> (Zdigits x + Zdigits y - 1 <= Zdigits (x * y))%Z.
proof: Proof. intros x y Zx Zy. cut ((Zdigits x - 1) + (Zdigits y - 1) < Zdigits (x * y))%Z. lia. apply Zdigits_gt_Zpower. rewrite Zabs_Zmult. rewrite Zpower_exp. apply Zmult_le_compat. apply Zpower_le_Zdigits. apply Zlt_pred. apply Zpower_le_Zdigits. apply Zlt_pred. apply Zpower_ge_0. apply Zpower_ge_0. generalize (Zdigits_gt_0 x). lia. generalize (Zdigits_gt_0 y). lia. Qed.
imports: Coq(Lia ZArith Zquot) Zaux