fact: Definition T_invsqrt x := P.rec1 (invsqrt_rec u x) (C.invsqrt u x).
imports: Coq(ZArith Reals) Flocq(Raux) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Interval Datatypes Basic_rec