proposition: Theorem FNoddEq : forall f1 f2 : float, Fbounded b f1 -> Fbounded b f2 -> f1 = f2 :>R -> FNodd f1 -> FNodd f2.
proof: Proof. intros f1 f2 H' H'0 H'1 H'2; red in |- *. rewrite FcanonicUnique with (3 := pGivesBound) (p := Fnormalize radix b precision f2) (q := Fnormalize radix b precision f1); auto with zarith arith. apply FnormalizeCanonic; auto with zarith. apply FnormalizeCanonic; auto with zarith. repeat rewrite FnormalizeCorrect; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz