proposition: Theorem CanonicFulp : forall p : float, Fcanonic radix b p -> Fulp p = Float 1 (Fexp p).
proof: Proof. intros p H; unfold Fulp in |- *. rewrite FcanonicFnormalizeEq; auto with zarith. unfold FtoRradix, FtoR in |- *; simpl in |- *; ring. Qed.
imports: Reals ZArith List PeanoNat Psatz