fact: Definition sqrt_rec (x : C.T) (a : C.T) (n : nat) := let nn := C.from_nat u n in let n1 := C.from_nat u n.-1 in let two := C.from_nat u 2 in (C.one - two * n1) * a / (two * x * nn).
imports: Coq(ZArith Reals) Flocq(Raux) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Interval Datatypes Basic_rec