proposition: Theorem FsubnormalUnique : forall p q : float, Fsubnormal p -> Fsubnormal q -> p = q :>R -> p = q.
proof: Proof. intros p q H' H'0 H'1. apply FtoREqInv2 with (radix := radix); auto. generalize H' H'0; unfold Fsubnormal in |- *; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz