proposition: Theorem ZOmod_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.rem (u + v) (Zpower beta n) = (Z.rem u (Zpower beta n) + Z.rem v (Zpower beta n))%Z.
proof: Proof. intros u v n Huv Hd. destruct (Zle_or_lt 0 n) as [Hn|Hn]. rewrite Zplus_rem with (1 := Huv). apply ZOmod_small_abs. generalize (Z.le_refl n). pattern n at -2 ; rewrite <- Z.abs_eq with (1 := Hn). rewrite <- (inj_Zabs_nat n). induction (Z.abs_nat n) as [|p IHp]. now rewrite 2!Z.rem_1_r. rewrite <- 2!Zsum_digit_digit. simpl Zsum_digit. rewrite inj_S. intros Hn'. replace (Zsum_digit (Zdigit u) p + Zdigit u (Z_of_nat p) * beta ^ Z_of_nat p + (Zsum_digit (Zdigit v) p + Zdigit v (Z_of_nat p) * beta ^ Z_of_nat p))%Z with (Zsum_digit (Zdigit u) p + Zsum_digit (Zdigit v) p + (Zdigit u (Z_of_nat p) + Zdigit v (Z_of_nat p)) * beta ^ Z_of_nat p)%Z by ring. apply (Z.le_lt_trans _ _ _ (Z.abs_triangle _ _)). replace (beta ^ Z.succ (Z_of_nat p))%Z with (beta ^ Z_of_nat p + (beta - 1) * beta ^ Z_of_nat p)%Z. apply Zplus_lt_le_compat. rewrite 2!Zsum_digit_digit. apply IHp. now apply Zle_succ_le. rewrite Zabs_Zmult. rewrite (Z.abs_eq (beta ^ Z_of_nat p)) by apply Zpower_ge_0. apply Zmult_le_compat_r. 2: apply Zpower_ge_0. apply Zlt_succ_le. assert (forall u v, Z.abs (Zdigit u v) < Z.succ (beta - 1))%Z. clear ; intros n k. assert (0 < beta)%Z. apply Z.lt_le_trans with 2%Z. apply refl_equal. apply Zle_bool_imp_le. apply beta. replace (Z.succ (beta - 1)) with (Z.abs beta). apply Zrem_lt. now apply Zgt_not_eq. rewrite Z.abs_eq. apply Zsucc_pred. now apply Zlt_le_weak. assert (0 <= Z_of_nat p < n)%Z. split. apply Zle_0_nat. apply Z.gt_lt. now apply Zle_succ_gt. destruct (Hd (Z_of_nat p) H0) as [K|K] ; rewrite K. apply H. rewrite Zplus_0_r. apply H. unfold Z.succ. ring_simplify. rewrite Zpower_plus. change (beta ^1)%Z with (beta * 1)%Z. now rewrite Zmult_1_r. apply Zle_0_nat. easy. destruct n as [|n|n] ; try easy. now rewrite 3!Zrem_0_r. Qed.
imports: Coq(Lia ZArith Zquot) Zaux