proposition: Theorem digitInv : forall (q : Z) (r : nat), (Zpower_nat n (pred r) <= Z.abs q)%Z -> (Z.abs q < Zpower_nat n r)%Z -> digit q = r.
proof: Proof. intros q r H' H'0; case (Nat.le_gt_cases (digit q) r). intros H'1; case (proj1 (Nat.lt_eq_cases _ _) H'1); auto; intros H'2. absurd (Z.abs q < Zpower_nat n (digit q))%Z; auto with zarith. apply Zle_not_lt; auto with zarith. apply Z.le_trans with (m := Zpower_nat n (pred r)); auto with zarith. apply Zpower_nat_monotone_le. generalize H'2; case r; auto with arith. apply digitMore. intros H'1. absurd (Zpower_nat n (pred (digit q)) <= Z.abs q)%Z; auto with zarith. apply Zlt_not_le; auto with zarith. apply Z.lt_le_trans with (m := Zpower_nat n r); auto. apply Zpower_nat_monotone_le. generalize H'1; case (digit q); auto with arith. apply digitLess; auto with zarith. generalize H'1; case q; unfold digit in |- *; intros tmp; intros; red in |- *; intros; try discriminate; contradict tmp; auto with arith. Qed.
imports: Reals ZArith List PeanoNat Psatz