proposition: Theorem ZOdiv_plus_pow_digit : forall u v n, (0 <= u * v)%Z -> (forall k, (0 <= k < n)%Z -> Zdigit u k = Z0 \/ Zdigit v k = Z0) -> Z.quot (u + v) (Zpower beta n) = (Z.quot u (Zpower beta n) + Z.quot v (Zpower beta n))%Z.
proof: Proof. intros u v n Huv Hd. rewrite <- (Zplus_0_r (Z.quot u (Zpower beta n) + Z.quot v (Zpower beta n))). rewrite ZOdiv_plus with (1 := Huv). rewrite <- ZOmod_plus_pow_digit by assumption. apply f_equal. destruct (Zle_or_lt 0 n) as [Hn|Hn]. apply ZOdiv_small_abs. rewrite <- Z.abs_eq. apply Zrem_lt. apply Zgt_not_eq. now apply Zpower_gt_0. apply Zpower_ge_0. clear -Hn. destruct n as [|n|n] ; try easy. apply Zquot_0_r. Qed.
imports: Coq(Lia ZArith Zquot) Zaux