proposition: Lemma mag_sqrt_F2R : forall m1 e1, (0 < m1)%Z -> mag beta (sqrt (F2R (Float beta m1 e1))) = Z.div2 (Zdigits beta m1 + e1 + 1) :> Z.
proof: Proof. intros m1 e1 Hm1. rewrite <- (mag_F2R_Zdigits beta m1 e1) by now apply Zgt_not_eq. apply mag_sqrt. now apply F2R_gt_0. Qed.
imports: Coq(ZArith Reals Lia) Zaux Raux Defs Digits Generic_fmt Float_prop Bracket