proposition: Theorem Zdigit_plus : forall u v, (0 <= u * v)%Z -> (forall k, (0 <= k)%Z -> Zdigit u k = Z0 \/ Zdigit v k = Z0) -> forall k, Zdigit (u + v) k = (Zdigit u k + Zdigit v k)%Z.
proof: Proof. intros u v Huv Hd k. destruct (Zle_or_lt 0 k) as [Hk|Hk]. unfold Zdigit. rewrite ZOdiv_plus_pow_digit with (1 := Huv). rewrite <- (Zmult_1_r beta) at 3 5 7. change (beta * 1)%Z with (beta ^1)%Z. apply ZOmod_plus_pow_digit. apply Zsame_sign_trans_weak with v. intros Zv ; rewrite Zv. apply Zquot_0_l. rewrite Zmult_comm. apply Zsame_sign_trans_weak with u. intros Zu ; rewrite Zu. apply Zquot_0_l. now rewrite Zmult_comm. apply Zsame_sign_odiv. apply Zpower_ge_0. apply Zsame_sign_odiv. apply Zpower_ge_0. intros k' (Hk1,Hk2). rewrite 2!Zdigit_div_pow by assumption. apply Hd. now apply Zplus_le_0_compat. intros k' (Hk1,Hk2). now apply Hd. now rewrite 3!Zdigit_lt. Qed.
imports: Coq(Lia ZArith Zquot) Zaux