proposition: Theorem FweightEq : forall p q : float, Fcanonic radix b p -> Fcanonic radix b q -> p = q :>R -> Fweight p = Fweight q.
proof: Proof. intros p q H' H'0 H'1. rewrite (FcanonicUnique _ radixMoreThanOne b precision) with (p := p) (q := q); auto with arith. Qed.
imports: Reals ZArith List PeanoNat Psatz