proposition: Theorem canonical_canonical_mantissa : forall (sx : bool) mx ex, canonical_mantissa mx ex = true -> canonical radix2 fexp (Float radix2 (cond_Zopp sx (Zpos mx)) ex).
proof: Proof. intros sx mx ex H. assert (Hx := Zeq_bool_eq _ _ H). clear H. apply sym_eq. simpl. pattern ex at 2 ; rewrite <- Hx. apply (f_equal fexp). rewrite mag_F2R_Zdigits. rewrite <- Zdigits_abs. rewrite Zpos_digits2_pos. now case sx. now case sx. Qed.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative