proposition: Lemma Uint63_sqrt_small : forall x, (Uint63.sqrt x <? min_int = true)%uint63.
proof: Proof. intros x. apply Uint63.ltb_spec. generalize (Uint63.sqrt_spec x), (Uint63.to_Z_bounded x). change wB with 9223372036854775808%Z. change (Uint63.to_Z min_int) with 4611686018427387904%Z. lia. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)