proposition: Theorem FulpComp : forall p q : float, Fbounded b p -> Fbounded b q -> p = q :>R -> Fulp p = Fulp q.
proof: Proof. intros p q H' H'0 H'1; unfold Fulp in |- *. rewrite FcanonicUnique with (p := Fnormalize radix b precision p) (q := Fnormalize radix b precision q) (3 := pGivesBound); auto with zarith. apply FnormalizeCanonic; auto with zarith. apply FnormalizeCanonic; auto with zarith. apply trans_eq with (FtoR radix p). apply FnormalizeCorrect; auto. apply trans_eq with (FtoR radix q); auto. apply sym_eq; apply FnormalizeCorrect; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz