proposition: Lemma size_TM_sub Mf Mg : Pol.size (approx (TM_sub Mf Mg)) = maxn (Pol.size (approx Mf)) (Pol.size (approx Mg)).
proof: Proof. by rewrite /TM_sub /= Pol.size_sub. Qed.
imports: Coq(ZArith Psatz Reals) Flocq(Raux) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Stdlib MathComp Coquelicot Xreal Interval Basic Xreal_derive Interval_compl Datatypes Taylor_poly Basic_rec Bound