proposition: Theorem digitAuxLess : forall (v r : Z) (q : positive), match digitAux v r q with | S r' => (Zpower_nat n r' * r <= v)%Z | O => True end.
proof: Proof. intros v r q; generalize r; elim q; clear r q; simpl in |- *; auto. intros q' Rec r; generalize (Zcompare_correct r v); case (r ?= v)%Z; auto. intros H1; generalize (Rec (n * r)%Z); case (digitAux v (n * r) q'). intros; rewrite H1; rewrite Zpower_nat_O; auto with zarith. intros r'; rewrite digitAux1; auto. intros H1; generalize (Rec (n * r)%Z); case (digitAux v (n * r) q'). intros; rewrite Zpower_nat_O; lia. intros r'; rewrite digitAux1; auto. intros q' Rec r; generalize (Zcompare_correct r v); case (r ?= v)%Z; auto. intros H1; generalize (Rec (n * r)%Z); case (digitAux v (n * r) q'). intros; rewrite H1; rewrite Zpower_nat_O; auto with zarith. intros r'; rewrite digitAux1; auto. intros H1; generalize (Rec (n * r)%Z); case (digitAux v (n * r) q'). intros; rewrite Zpower_nat_O; lia. intros r'; rewrite digitAux1; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz