proposition: Lemma splitf (n : nat) (e : F) : e = iterop n +%R (e / n%:R) e.
proof: Proof. case: n=> // n; set e' := (e / _). have -> : e = e' * n.+1%:R by rewrite mulfVK ?pnatr_eq0. move: e'=> {}e; rewrite iteropS. by elim: n=> /= [|n <-]; rewrite !mulr_natr ?mulr1n. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(bigop order ssralg ssrnum ssrint rat poly polydiv polyorder) mathcomp(perm matrix mxpoly polyXY binomial bigenough)