fact: Definition cos_rec (a b : C.T) (n : nat) : C.T := C.div u (C.opp a) (C.mul u (C.from_nat u n) (C.from_nat u n.-1)).
imports: Coq(ZArith Reals) Flocq(Raux) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Interval Datatypes Basic_rec