proposition: Theorem Zdigits_mult_strong : forall x y, (0 <= x)%Z -> (0 <= y)%Z -> (Zdigits (x + y + x * y) <= Zdigits x + Zdigits y)%Z.
proof: Proof. intros x y Hx Hy. apply Zdigits_le_Zpower. rewrite Z.abs_eq. apply Z.lt_le_trans with ((x + 1) * (y + 1))%Z. ring_simplify. apply Zle_lt_succ, Z.le_refl. rewrite Zpower_plus by apply Zdigits_ge_0. apply Zmult_le_compat. apply Zlt_le_succ. rewrite <- (Z.abs_eq x) at 1 by easy. apply Zdigits_correct. apply Zlt_le_succ. rewrite <- (Z.abs_eq y) at 1 by easy. apply Zdigits_correct. clear -Hx ; lia. clear -Hy ; lia. change Z0 with (0 + 0 + 0)%Z. apply Zplus_le_compat. now apply Zplus_le_compat. now apply Zmult_le_0_compat. Qed.
imports: Coq(Lia ZArith Zquot) Zaux