proposition: Theorem boundNatCorrect : forall n : nat, (n < boundNat n)%R.
proof: Proof. intros n; unfold FtoRradix, FtoR, boundNat in |- *; simpl in |- *. rewrite Rmult_1_l. rewrite <- Zpower_nat_Z_powerRZ; auto with real zarith. apply Rle_lt_trans with (Z.abs n); [rewrite (Z.abs_eq (Z_of_nat n))|idtac];auto with real zarith. apply IZR_lt, digitMore; easy. Qed.
imports: Reals ZArith List PeanoNat Psatz