proposition: Lemma equivFloat_Sqrt_Integer {Tl} : forall (t : ArithExpr Tl Integer) (lC : evalExprTypeFloat_list Tl) md, let lM := C2M_list lC in eqExprTypeFloat (evalFloat t lC md) (evalRounded t lM md) -> (0 <= evalRounded t lM md)%Z -> eqExprTypeFloat (evalFloat (Sqrt t) lC md) (evalRounded (Sqrt t) lM md).
proof: Proof. intros t lC md lM [bndt eqt] nonnegt. unfold eqExprTypeFloat. simpl. rewrite eqt in bndt. rewrite eqt. split; [| easy]. clear -bndt nonnegt. revert bndt. unfold convertibleFloat, Int32.in_bounds. generalize (Z.sqrt_spec (evalRounded t lM md) nonnegt). simpl. lia. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)