proposition: Theorem digitAuxMore : forall (v r : Z) (q : positive), (0 < r)%Z -> (v < Zpower_nat n (pos_length q) * r)%Z -> (v < Zpower_nat n (digitAux v r q) * r)%Z.
proof: Proof. intros v r q; generalize r; elim q; clear r q; simpl in |- *. intros p Rec r Hr; generalize (Zcompare_correct r v); case (r ?= v)%Z; auto. intros H1 H2; rewrite <- H1. apply Z.le_lt_trans with (Zpower_nat n 0 * r)%Z; auto with zarith arith. rewrite Zpower_nat_O; rewrite Zmult_1_l; auto with zarith. apply Zmult_lt_compat_r; auto with zarith. apply Zpower_nat_monotone_lt; auto with zarith. intros H1 H2; rewrite digitAux1. apply Rec. apply Z.mul_pos_pos; auto with zarith. rewrite <- digitAux1; auto. rewrite Zpower_nat_O; rewrite Zmult_1_l; auto with zarith. intros p Rec r Hr; generalize (Zcompare_correct r v); case (r ?= v)%Z; auto. intros H1 H2; rewrite <- H1. apply Z.le_lt_trans with (Zpower_nat n 0 * r)%Z; auto with zarith arith. rewrite Zpower_nat_O; rewrite Zmult_1_l; auto with zarith. apply Zmult_lt_compat_r; auto with zarith. apply Zpower_nat_monotone_lt; auto with zarith. intros H1 H2; rewrite digitAux1. apply Rec. apply Z.mul_pos_pos; auto with zarith. rewrite <- digitAux1; auto. rewrite Zpower_nat_O; rewrite Zmult_1_l; auto with zarith. auto. Qed.
imports: Reals ZArith List PeanoNat Psatz