proposition: Theorem canonical_unique : forall f1 f2, canonical f1 -> canonical f2 -> F2R f1 = F2R f2 -> f1 = f2.
proof: Proof. intros (m1, e1) (m2, e2). unfold canonical. simpl. intros H1 H2 H. rewrite H in H1. rewrite <- H2 in H1. clear H2. rewrite H1 in H |- *. apply (f_equal (fun m => Float beta m e2)). apply eq_F2R with (1 := H). Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Round_pred Float_prop