proposition: Theorem FnormalUnique : forall p q : float, Fnormal p -> Fnormal q -> p = q :>R -> p = q.
proof: Proof. intros p q H' H'0 H'1. apply (FdigitEq radix); auto. apply FnormalNotZero; auto. apply trans_equal with (y := precision). now apply FnormalPrecision. now apply sym_equal, FnormalPrecision. Qed.
imports: Reals ZArith List PeanoNat Psatz