proposition: Lemma periodicn f (T : U) : periodic f T -> forall n a, f (a + T *+ n) = f a.
proof: Proof. by move=> fT; elim=> [|n ih] a;[rewrite mulr0n addr0|rewrite mulrS addrA ih fT]. 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