proposition: Lemma equivPrim_Sqrt_Integer {Tl} : forall (t : ArithExpr Tl Integer) (lP : evalExprTypePrim_list Tl), let lM := P2M_list lP in eqExprTypePrim (evalPrim t lP) (evalRounded t lM mode_NE) -> (0 <= evalRounded t lM mode_NE)%Z -> eqExprTypePrim (evalPrim (Sqrt t) lP) (evalRounded (Sqrt t) lM mode_NE).
proof: Proof. intros t lP lM [bndt eqt] nonnegt. unfold eqExprTypePrim. simpl in *. rewrite eqt in bndt. rewrite <-eqt in bndt, nonnegt |- *. change 0%Z with (to_Z 0) in nonnegt. apply Sint63.leb_spec in nonnegt. unfold to_Z. rewrite lesb_ltb in nonnegt. rewrite nonnegt, Uint63_sqrt_small. split; [| apply Uint63_to_Z_sqrt]. unfold to_Z in bndt. rewrite nonnegt in bndt. unfold convertiblePrim, Int32.in_bounds in bndt. simpl in bndt. apply in_bounds_to_Z_Uint63_sqrt. lia. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)