proposition: Theorem Zdigits_mult : forall x y, (Zdigits (x * y) <= Zdigits x + Zdigits y)%Z.
proof: Proof. intros x y. rewrite <- Zdigits_abs. rewrite <- (Zdigits_abs x). rewrite <- (Zdigits_abs y). apply Z.le_trans with (Zdigits (Z.abs x + Z.abs y + Z.abs x * Z.abs y)). apply Zdigits_le. apply Zabs_pos. rewrite Zabs_Zmult. generalize (Zabs_pos x) (Zabs_pos y). lia. apply Zdigits_mult_strong ; apply Zabs_pos. Qed.
imports: Coq(Lia ZArith Zquot) Zaux