proposition: Theorem NotDividesDigit : forall r v : Z, (1 < r)%Z -> v <> 0%Z -> ~ Zdivides v (Zpower_nat r (digit r v)).
proof: Proof. intros r v H H'; red in |- *; intros H'0; case H'0; intros q E. absurd (Z.abs v < Zpower_nat r (digit r v))%Z; auto with zarith. apply Zle_not_lt. case (Z.eq_dec q 0); intros Z1. case H'; rewrite E; rewrite Z1; ring. pattern v at 2 in |- *; rewrite E. rewrite Zabs_Zmult. pattern (Zpower_nat r (digit r v)) at 1 in |- *; replace (Zpower_nat r (digit r v)) with (Zpower_nat r (digit r v) * 1)%Z; [ idtac | ring ]. rewrite (fun x y => Z.abs_eq (Zpower_nat x y)); auto with zarith. apply Zle_Zmult_comp_l; try lia. apply Zpower_NR0; lia. apply Zpower_NR0; lia. now apply digitMore. Qed.
imports: Reals ZArith List PeanoNat Psatz