proposition: Lemma alternatingn f (T : U) : alternating f T -> forall n a, f (a + T *+ n) = (- 1) ^+ n * f a.
proof: Proof. move=> fT; elim => [a|n ih a]; first by rewrite mulr0n expr0 addr0 mul1r. by rewrite mulrS addrA ih fT exprS mulrN mulN1r mulNr. Qed.
imports: mathcomp(all_ssreflect ssralg ssrint ssrnum matrix) mathcomp(interval rat) mathcomp(mathcomp_extra boolp classical_sets functions) reals ereal nsatz_realtype signed topology normedtype landau sequences derive realfun exp