proposition: Theorem spec_sqrt: forall x, [sqrt x] = Z.sqrt [x].
proof: Proof. intros x. symmetry. apply Z.sqrt_unique. rewrite <- ! Z.pow_2_r. apply spec_sqrt_aux. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen