proposition: Theorem FcanonicUnique : forall p q : float, Fcanonic p -> Fcanonic q -> p = q :>R -> p = q.
proof: Proof. intros p q H' H'0 H'1; case H'; case H'0; intros H'2 H'3. apply FnormalUnique; auto. contradict H'1; apply NormalAndSubNormalNotEq; auto. absurd (q = p :>R); auto; apply NormalAndSubNormalNotEq; auto. apply FsubnormalUnique; auto. Qed.
imports: Reals ZArith List PeanoNat Psatz