proposition: Theorem FcanonicFnormalizeEq : forall p : float, Fcanonic p -> Fnormalize p = p.
proof: Proof. intros p H'. apply FcanonicUnique; auto. apply FnormalizeCanonic; auto. apply FcanonicBound with (1 := H'); auto. apply FnormalizeCorrect; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz