fact: Definition T_tan x := let polyX := P.lift 1 P.one in let J := C.tan u x in let s := [::] in let F q n := let q' := P.deriv u q in P.div_mixed_r u (P.add u q' (P.lift 2 q')) (C.from_nat u n) in let G q _ := P.horner u q J in P.grec1 F G polyX s.
imports: Coq(ZArith Reals) Flocq(Raux) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Interval Datatypes Basic_rec