proposition: Lemma Uint63_to_Z_sqrt : forall x, Uint63.to_Z (Uint63.sqrt x) = Z.sqrt (Uint63.to_Z x).
proof: Proof. intros x. generalize (Uint63.sqrt_spec x). rewrite 2Z.pow_2_r. intros H. symmetry. now apply Z.sqrt_unique. Qed.
imports: Coq(PrimInt63 Sint63 Floats PArray) Coq(Bool List Reals Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations)