proposition: Theorem firstNormalPos_eq : FtoRradix (firstNormalPos radix b p) = powerRZ radix (Z.pred p + - dExp b).
proof: Proof. unfold firstNormalPos, nNormMin, FtoRradix, FtoR in |- *; simpl. rewrite Zpower_nat_Z_powerRZ; rewrite powerRZ_add; try apply IZR_neq; auto with real zarith. replace (Z_of_nat (pred p)) with (Z.pred p); [ ring | rewrite inj_pred; auto with zarith ]. Qed.
imports: Reals ZArith List PeanoNat Psatz