proposition: Lemma in_bounds_to_Z_Uint63_sqrt : forall x, (Uint63.to_Z x <= 2 ^ 62 - 1)%Z -> Int32.in_bounds (Uint63.to_Z (Uint63.sqrt x)).
proof: Proof. intros x H0. generalize (Uint63.sqrt_spec x), (Uint63.to_Z_bounded x). rewrite Uint63_to_Z_sqrt. change wB with 9223372036854775808%Z. intros [H1 _] H2. unfold Int32.in_bounds. simpl. lia. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)