proposition: Theorem Zdigit_ext : forall n1 n2, (forall k, (0 <= k)%Z -> Zdigit n1 k = Zdigit n2 k) -> n1 = n2.
proof: Proof. intros n1 n2 H. rewrite <- (ZOmod_small_abs n1 (Zpower beta (Z.max (Z.abs n1) (Z.abs n2)))). rewrite <- (ZOmod_small_abs n2 (Zpower beta (Z.max (Z.abs n1) (Z.abs n2)))) at 2. replace (Z.max (Z.abs n1) (Z.abs n2)) with (Z_of_nat (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2)))). rewrite <- 2!Zsum_digit_digit. induction (Z.abs_nat (Z.max (Z.abs n1) (Z.abs n2))). easy. simpl. rewrite H, IHn. apply refl_equal. apply Zle_0_nat. rewrite inj_Zabs_nat. apply Z.abs_eq. apply Z.le_trans with (Z.abs n1). apply Zabs_pos. apply Z.le_max_l. apply Z.lt_le_trans with (Zpower beta (Z.abs n2)). apply Zpower_gt_id. apply Zpower_le. apply Z.le_max_r. apply Z.lt_le_trans with (Zpower beta (Z.abs n1)). apply Zpower_gt_id. apply Zpower_le. apply Z.le_max_l. Qed.
imports: Coq(Lia ZArith Zquot) Zaux