diff --git a/expansiblefracpoly.v b/expansiblefracpoly.v
index c9f028b..bab4fee 100644
--- a/expansiblefracpoly.v
+++ b/expansiblefracpoly.v
@@ -33,7 +33,7 @@ Variable K : fieldType.
 Definition fracpoly_of of phant K := {fracpoly K}.
 Notation "{ 'fracpoly' K }" := (fracpoly_of (Phant K)).
 
-Definition devs : pred_class := fun f : {fracpoly K} => (~~ (0.-fppole) f).
+Definition devs := fun f : {fracpoly K} => (~~ (0.-fppole) f).
 
 Lemma devs_invf (p : {poly K}) : p != 0 -> (0.-fppole) p%:F^-1 = (p`_0 == 0).
 Proof. by move => p_neq0; rewrite fpoleV -horner_coef0 froot_tofrac. Qed.
@@ -80,6 +80,12 @@ Proof. by move => dx dy; rewrite devsD // devsN. Qed.
 
 Variable n : nat.
 
+Notation Tfpsp := trXn.
+
+Lemma Tfpsp_is_unit (p : {poly K}) :
+  ((Tfpsp n p) \is a GRing.unit) = (p`_0 != 0).
+Proof. by rewrite unit_tfpsE unitfE coef0_trXn. Qed.
+
 Definition Tfpsfp (x : {fracpoly K}) :=
   if (0.-fppole) x then 0
   else let (x1, x2) := projT1 (fracpolyE x) in (Tfpsp n x1) / (Tfpsp n x2).
@@ -111,7 +117,7 @@ have v0_neq0 : v`_0 != 0.
     apply/negbTE; move: q0_neq0; apply/contra.
     exact: devs_frac.
   by [].
-apply/eqP ; rewrite eq_divr ?Tfpsp_is_unit // -!rmorphM.
+apply/eqP; rewrite (@eq_divr _ (Tfpsp n u)) ?Tfpsp_is_unit // -!rmorphM.
 apply/eqP ; apply: (congr1 _) ; apply/eqP.
 apply/eqP/tofrac_inj/eqP.
 rewrite !rmorphM /= -eq_divf ?raddf_eq0 //; last 2 first.
@@ -237,8 +243,8 @@ Proof.
 move: (fracpolyE x) => [ [u v] /= Hx ] /andP [ v_neq0 coprime_u_v ].
 rewrite Hx fmorph_div /= !map_fracE /=.
 have [ v0_eq0 | v0_neq0 ] := eqVneq v`_0 0; last first.
-+ rewrite Tfpsfp_frac // Tfpsfp_frac; last first.
+- rewrite Tfpsfp_frac // Tfpsfp_frac; last first.
     by rewrite coef_map raddf_eq0 //; apply: fmorph_inj.
-+ by rewrite rmorph_div /= ?Tfpsp_is_unit // !Tfps_map_poly. 
-by rewrite !Tfpsfp_eq0 // ?coef_map ?v0_eq0 /= ?rmorph0 // coprimep_map. 
-Qed.
\ No newline at end of file
+- by rewrite rmorph_div /= ?Tfpsp_is_unit // !trXn_map_poly.
+by rewrite !Tfpsfp_eq0 // ?coef_map ?v0_eq0 /= ?rmorph0 // coprimep_map.
+Qed.
diff --git a/newtonsum.v b/newtonsum.v
index 3ac5bfa..905ff17 100644
--- a/newtonsum.v
+++ b/newtonsum.v
@@ -27,13 +27,14 @@ Unset Printing Implicit Defensive.
 Import GRing.Theory.
 Local Open Scope ring_scope.
 Local Open Scope quotient_scope.
-Local Open Scope tfps_scope.
 
 Local Notation "x =p y"  := (perm_eq x y) (at level 70, no associativity).
 
-Local Notation "p ^^ f" := (map_frac f p)  (f at next level, at level 30).
 Local Notation "p ^^^ f" := (map_frac (map_poly f) p)
-                              (f at next level, at level 30). 
+                              (f at next level, at level 30).
+
+Local Notation Tfpsp := trXn.
+
 
 Section MoreBigop.
 
@@ -95,7 +96,8 @@ Proof. by rewrite -[0](rmorph0 iota); apply: fppole_map. Qed.
 
 End PolynomialFractions.
 
-Import truncpowerseries.Notations.
+(* Import truncpowerseries.Notations. *)
+Local Open Scope tfps_scope.
 
 Section NewtonRepresentation.
 
@@ -156,17 +158,19 @@ have Hunit: (Tfpsp m (1 - a *: 'X)) \is a GRing.unit.
   by rewrite Tfpsp_is_unit coefB coefC coefZ coefX mulr0 subr0 oner_neq0. 
 apply: (mulrI Hunit); rewrite divrr; last first.
   by rewrite Tfpsp_is_unit coefB coefC coefZ coefX mulr0 subr0 oner_neq0. 
-apply/val_inj=> /=; rewrite modp_mul2.
+apply/val_inj=> /=.
+rewrite -!trXn_modE modp_mul2 trXn_modE.
 rewrite mulrBl mul1r /=; apply/polyP=> i.
-rewrite coef_modXn !poly_def mulr_sumr /=.
+rewrite coef_trXn !poly_def mulr_sumr /=.
 rewrite [X in _ - X](eq_bigr (fun i => a ^+ (nat_of_ord i).+1 *: 
                                               'X^(nat_of_ord i).+1)); last first.
   by move=> j _; rewrite -scalerAr -scalerAl scalerA -exprS -exprSr.
 rewrite -opprB -sumrB. 
 rewrite -(big_mkord predT (fun i => a ^+ i.+1 *: 'X^i.+1 - a ^+ i *: 'X^i)) /=.
 rewrite telescope_sumr // opprB coefB !coefZ !expr0 mul1r coefXn.
-have [|] := ltnP; last by rewrite coefC; case: i.
-by rewrite ltn_neqAle => /andP [ /negbTE -> _]; rewrite mulr0 subr0. 
+rewrite coef1; have [|] := ltnP; case: i => [|i] //=.
+  by rewrite mulr0 subr0.
+by rewrite ltn_neqAle eqSS => /andP [ /negbTE -> _]; rewrite mulr0 subr0.
 Qed.
 
 End Variable_m.
@@ -461,24 +465,23 @@ rewrite (big_morph_in (@devsD _) _ (@TfpsfpD _ _) (@Tfpsfp0 _ _)); last 2 first.
 - exact: rpred0.
 - apply/allP => x /=; move/mapP; rewrite filter_predT; move=> [y hy ->].
   exact: devs_inv1subCX.
-apply/eq_tfps => i /=; rewrite coef_poly ltn_ord /=.
+apply/tfpsP => i /= le_im; rewrite coef_poly ltnS le_im.
 rewrite (@big_morph _ _ (fun (x : {tfps L m}) => x`_i) 0 +%R); last 2 first.
 - by move => x y; apply: coefD.
 - exact: coef0.
-by apply: eq_bigr => x _; rewrite geometric_series /= coef_poly ltn_ord.
+by apply: eq_bigr => x _; rewrite geometric_series /= coef_poly ltnS le_im.
 Qed.
 
 Lemma map_poly_tfps m (s : {tfps K m}) :
   map_poly f (val s) = val (s ^ f).
-Proof.
-by rewrite /= modp_small // size_polyXn ltnS size_map_poly size_tfps.
-Qed.
+Proof. by []. Qed.
 
 Lemma newton_tfps_coef0 (p : {poly K}) (m : nat) :
     (newton_tfps m p)`_0 = ((size p).-1)%:R.
 Proof.
 apply: (@rmorph_inj _ _ f).
-rewrite -coef_map map_poly_tfps iota_newton_tfps coef_tfps /=.
+rewrite -coef_map map_poly_tfps iota_newton_tfps coef_tfps.
+rewrite coef_tfps_of_fun /=.
 rewrite rmorph_nat -iroots_size -sum1_size natr_sum.
 by apply: eq_bigr => r; rewrite expr0.
 Qed.
@@ -504,8 +507,9 @@ Lemma nth_newton_tfps (p : {poly L}) (m i : nat) :
   (newton_tfps m p)`_i = if i < m.+1 then
   (\sum_(r <- iroots [injmorphism of idfun] p) r ^+i) else 0.
 Proof.
+rewrite coef_tfpsE.
 have -> : val (newton_tfps m p) = 
-                            map_tfps [injmorphism of (@idfun L)] (newton_tfps m p).
+       tfps (map_tfps [injmorphism of (@idfun L)] (newton_tfps m p)).
   by rewrite -map_poly_tfps map_poly_id.
 by rewrite iota_newton_tfps //= coef_poly.
 Qed.
@@ -552,14 +556,14 @@ have [q_eq0 | q_neq0] := eqVneq q 0.
   exact: newton_tfps0.
 have -> : newton_tfps m (cmul f p q) =
     newton_tfps m (cmul f p q) ^ [rmorphism of (@idfun L)].
-  by rewrite (@map_powerseries_idfun _ _).
-rewrite (@map_powerseries_idfun _ _) /=.
-rewrite map_hmul !iota_newton_tfps //; apply/eq_tfps => i /=.
-rewrite !coef_poly ltn_ord.
+  by rewrite map_tfps_idfun.
+rewrite map_tfps_idfun /=.
+rewrite map_hmul !iota_newton_tfps //.
+apply/tfpsP => i /= le_im.
+rewrite !coef_poly ltnS le_im.
 rewrite (big_distrl _ _ _) /=.
-rewrite nth_newton_tfps ltn_ord.
-rewrite (eq_big_perm [seq s * t | s <- iroots f p, t <- iroots f q])
-                                                                    ; last first.
+rewrite nth_newton_tfps ltnS le_im.
+rewrite (eq_big_perm [seq s * t | s <- iroots f p, t <- iroots f q]); last first.
 exact: iroots_cmul.
 rewrite /= eq_big_allpairs /=.
 apply: eq_bigr => j _ ; rewrite (big_distrr _ _ _) /=.
@@ -571,33 +575,36 @@ Definition expX (K' : fieldType) (m : nat) := exp (Tfpsp m ('X : {poly K'})).
 
 Lemma expX0 (K' : fieldType) : expX K' 0%N = 1.
 Proof.
-rewrite -exp0; congr exp; apply/eq_tfps => i /=.
-by rewrite expr1 modpp.
+rewrite -exp0; congr exp; apply/tfpsP => i /=.
+rewrite leqn0 => /eqP ->.
+by rewrite coef0 coef_trXn coefX.
 Qed.
 
 Lemma nth_expX (K' : fieldType) (m i : nat) : 
   (expX K' m)`_i = if i < m.+1 then i`!%:R^-1 else 0.
 have [->|m_neq0] := eqVneq m O.
-  case:i => [|i]; last by rewrite tfps_nth_default.
-  by rewrite coef0_exp ?fact0 ?invr1 // coef0_is_0E coef_Tfpsp coefX.
-rewrite /expX /exp coef0_is_0E coef_Tfpsp coefX eqxx /= coef_modXn.
-rewrite (eq_bigr (fun i => (nat_of_ord i)`!%:R^-1 *: 
-                                              'X ^+ (nat_of_ord i))); last first.
-  by move => j _; rewrite modp_small // size_polyX size_polyXn !ltnS lt0n.
-by rewrite -(@poly_def _ _ (fun i => i`!%:R^-1))  coef_poly; case: (_ < _).
+  case: i => [|i]; last by rewrite coef_tfps ltn0.
+  by rewrite coef0_exp ?fact0 ?invr1 // coef0_eq0E coef_trXn coefX.
+rewrite /expX /exp coef0_eq0E coef_trXn coefX eqxx /= coef_tfps ltnS.
+rewrite coef_tfpsE raddf_sum.
+rewrite (eq_bigr (fun i : 'I_m.+1 => i`!%:R^-1 *: 'X ^+ i)); last first.
+  move => j _ /=.
+  by rewrite -rmorphX /= trXnK // size_polyXn ltn_ord.
+by rewrite -(@poly_def _ _ (fun i => i`!%:R^-1)) coef_poly ltnS; case: (_ <= _).
 Qed.
 
 (* can be generalized to (exp f) ^ iota = exp (f ^ iota) *)
 Lemma map_iota_expX (m : nat) : expX K m ^ f = expX L m.
 Proof.
-rewrite /expX /exp !coef0_is_0E !nth0_Tfpsp !coefX !eqxx -Tfps_map_poly. 
-rewrite rmorph_sum; congr Tfpsp; apply: eq_bigr => i _.
+rewrite /expX /exp !coef0_eq0E !coef0_trXn !coefX !eqxx /=.
+rewrite rmorph_sum /=; apply: eq_bigr => i _.
 rewrite linearZ ; congr (_ *: _).
   by rewrite rmorphV ?rmorph_nat // unitfE natmul_inj // -lt0n fact_gt0.
-by rewrite rmorphX /= map_modp map_polyX map_polyXn.
+  rewrite !rmorphX /=.
+by rewrite -trXn_map_poly map_polyX.
 Qed.
 
-Lemma hmul_tfps_p_expX (K' : fieldType) (m : nat ) (p : {tfps K' m}) : 
+Lemma hmul_tfps_p_expX (K' : fieldType) (m : nat ) (p : {tfps K' m}) :
   hmul_tfps p (expX K' m) = [tfps i => p`_i / i`!%:R].
 Proof.
 apply/val_inj => /=.
@@ -607,7 +614,7 @@ by case: (i < m.+1).
 Qed.
 
 Lemma aux_newton_cadd (K' : fieldType) (g : {rmorphism K' -> L}) 
-  (m : nat) (s t : seq K') (p : {tfps K' m}) : p \in (@coef0_is_0 K' m) ->
+  (m : nat) (s t : seq K') (p : {tfps K' m}) : p \in (@coef0_eq0 K' m) ->
   \sum_(w <- [seq u + v | u <- s, v <- t]) (exp (w *: p)) = 
   (\sum_(u <- s) (exp (u *: p))) * (\sum_(v <- t) (exp (v *: p))).
 Proof.
@@ -619,19 +626,14 @@ have H : [char K'] =i pred0.
 rewrite eq_big_allpairs /=.
 have -> : \sum_(i <- s) \sum_(j <- t) exp ((i + j) *: p) =
    \sum_(i <- s) \sum_(j <- t) (exp (i *: p)) * (exp (j *: p)).
-  apply: eq_bigr => i _.
-  apply: eq_bigr => j _.
-  rewrite scalerDl exp_is_morphism // ; rewrite -mulr_algr mulrC.
-  apply: (@idealMr _ _ (prime_idealr_zmod (coef0_is_0_pideal K' m)) 
-                                            (c0_is_0_keyed K' m) i%:A p) => //.
-  apply: (@idealMr _ _ (prime_idealr_zmod (coef0_is_0_pideal K' m)) 
-                                            (c0_is_0_keyed K' m) j%:A p) => //.
+  apply: eq_bigr => i _; apply: eq_bigr => j _.
+  by rewrite scalerDl expD // -mulr_algr mulrC idealMr.
 rewrite exchange_big /= mulr_sumr.
 apply: eq_big => // i _.
-by  rewrite mulr_suml.
+by rewrite mulr_suml.
 Qed.
 
-Lemma sum_exp_kX (m : nat) (p : {poly L}) : 
+Lemma sum_exp_kX (m : nat) (p : {poly L}) :
   hmul_tfps (newton_tfps m.+1 p) (expX L m.+1) = 
   \sum_(r <- iroots [injmorphism of @idfun L] p) (exp (r *: (@Tfpsp L m.+1 'X))).
 Proof.
@@ -661,19 +663,16 @@ have -> : \sum_(i < m.+2)
   by rewrite polyC1 unitrE divr1.
   by rewrite -scalerAr divr1 scalerA mulrC.
 rewrite exchange_big /=.
-rewrite (@big_morph _ _ (fun (x : {tfps L m.+1}) => val x) 0 +%R) //=. 
+rewrite (@big_morph _ _ (fun (x : {tfps L m.+1}) => val x) 0 +%R) //=.
 apply: eq_big => //= x _.
-rewrite exp_coef0_is_0; last first.
-  by rewrite coef0_is_0E coef_modXn coefZ nth0_Tfpsp coefX /= mulr0. 
-rewrite rmorph_sum /=.
-rewrite (@big_morph _ _ (fun (x : {tfps L m.+1}) => val x) 0 +%R) //=. 
-apply: eq_big => //= i _.
-rewrite ['X %% _]modp_small ?size_polyX ?size_polyXn //.
-rewrite modp_scalel ['X %% _]modp_small ?size_polyX ?size_polyXn //.
-rewrite modp_scalel modp_small; last first.
-  rewrite size_polyXn exprZn (leq_ltn_trans (size_scale_leq _ _)) //.
-  by rewrite size_polyXn ltnS.
-by rewrite mulrC -raddfMn polyC_inv mul_polyC.
+rewrite exp_coef0_eq0; last first.
+  by rewrite coef0_eq0E coefZ coef0_trXn coefX /= mulr0.
+rewrite raddf_sum /=; apply: eq_bigr => //= i _.
+rewrite mulrC -scaler_nat -in_algE -rmorphV ?fact_unit //= mulr_algl.
+congr (_ *: _).
+rewrite -linearZ -rmorphX /= trXnK //.
+rewrite exprZn; apply: (leq_trans (size_scale_leq _ _)).
+by rewrite size_polyXn ltn_ord.
 Qed.
 
 Lemma newton_cadd (p q : {poly K}) :
@@ -687,23 +686,19 @@ move => p_neq0 q_neq0 /=.
 set m := ((size p).-1 * (size p).-1)%N.
 case: m => [|m].
   rewrite !expX0; apply/val_inj => /=.
-  rewrite expr1 map_modp map_polyX rmorphM !poly_def.
-  rewrite !big_ord_recr !big_ord0 !Monoid.simpm.
-  rewrite !expr0 !coefC eqxx !mulr1. 
+  rewrite !poly_def !big_ord_recr !big_ord0 !Monoid.simpm /= -!/(_`_0).
   rewrite !(newton_tfps_coef0 [injmorphism of (@idfun L)]) //.
-  rewrite !(newton_tfps_coef0 f) //=.
-  rewrite size_cadd // natrM !linearZ /=.
-  rewrite rmorph1 !rmorph_nat mulr_algr scalerA mulrC expr1 modp_mod.
-  rewrite modp_small // size_polyX (leq_ltn_trans (size_scale_leq _ _)) //.
-  rewrite size_polyC.
-  exact: leq_b1.
+  rewrite coef1 mulr1 expr0 size_cadd // scaler_nat.
+  rewrite !hmul_tfpsr1 !(newton_tfps_coef0 f) //=.
+  rewrite -tfpsCM -natrM -alg_tfpsC scaler_nat.
+  by rewrite !raddfMn /= rmorph1.
 rewrite rmorphM /= !map_hmul map_iota_expX !newton_tfps_map_iota.
-rewrite !sum_exp_kX. 
+rewrite !sum_exp_kX.
 rewrite (eq_big_perm [seq s + t | s <- iroots f p, t <- iroots f q]) /= ;
   last exact: iroots_cadd.
 rewrite !iroots_idfun.
 apply: (aux_newton_cadd [rmorphism of @idfun L]).
-by rewrite coef0_is_0E nth0_Tfpsp coefX [in X in X == _]eq_sym. 
+by rewrite coef0_eq0E coef0_trXn coefX [in X in X == _]eq_sym. 
 Qed.
 
 Fact aux_conversion1 (p : {poly K}) : ~~ (root p 0) ->
@@ -735,7 +730,7 @@ Qed.
 (* to generalize ? *)
 Fact aux_conversion2 (m : nat) (p : {poly K}) :
   ~~ (root p 0) ->
-  Tfpsfp m (((revp p)^`() // revp p) ^^^ f) = 
+  Tfpsfp m (((revp p)^`() // revp p) ^^^ f) =
   - [tfps i => \sum_(r <- iroots f p) r ^+i.+1].
 Proof.
 move => zeroNroot.
@@ -750,15 +745,15 @@ rewrite (big_morph_in (@devsD _) _ (@TfpsfpD _ _) (@Tfpsfp0 _ _)); last 2 first.
   apply: devsM.
     by rewrite /devs fpole_tofrac.
     exact: devs_inv1subCX.
-apply/eq_tfps => i /=; rewrite coef_poly ltn_ord.
+apply/tfpsP => i /= le_im; rewrite coef_poly ltnS le_im.
 rewrite (@big_morph _ _ (fun (x : {tfps L m}) => x`_i) 0 +%R); last 2 first.
 - by move => x y; apply: coefD.
 - exact: coef0.
 apply: eq_bigr => x _; rewrite TfpsfpM -?topredE /= ; last 2 first.
 - by rewrite /devs fpole_tofrac.
 - exact: devs_inv1subCX.
-rewrite coef_modXn ltn_ord geometric_series Tfpsfp_tofrac /=.
-by rewrite modCXn // mul_polyC coefZ coef_poly ltn_ord -exprS.
+rewrite coef_trXn le_im geometric_series Tfpsfp_tofrac /=.
+by rewrite trXnC mul_polyC coefZ coef_poly ltnS le_im -exprS.
 Qed.
 
 End Conversion.
@@ -781,31 +776,29 @@ Proof.
 move => zeroNroot.
 apply: (@map_tfps_injective _ _ m' f).
 rewrite map_Tfpsfp aux_conversion2 // (@map_tfps_divfX _ _ f m'.+1).
-rewrite divfXE; last first.
-  rewrite coef0_is_0E -map_poly_tfps coef_map coefB nth0_Tfpsp //.
-  by rewrite (newton_tfps_coef0 f) // coefC /= subrr rmorph0.
-apply/eq_tfps => i.
-rewrite coefN !coef_poly ltn_ord rmorphB coefB [X in X`_i.+1]/=.
+apply/tfpsP => i le_im'.
+rewrite coef_divfX coefN coef_poly ltnS le_im'.
+rewrite rmorphB coefB -!coef_tfpsE /= -!/(_`_i.+1).
 rewrite [X in val X]/=  newton_tfps_map_iota nth_newton_tfps //.
-rewrite ltnS ltn_ord map_modp map_polyXn modp_mod modp_small; last first.
-  by rewrite size_map_poly size_polyC size_polyXn (leq_ltn_trans (leq_b1 _)).
-by rewrite coef_map coefC /= rmorph0 sub0r /iroots map_poly_id.
+rewrite !ltnS le_im'.
+rewrite coef_map coef_tfpsC /= rmorph0 sub0r.
+by rewrite iroots_idfun.
 Qed.
 
 Lemma exp_prim_derivp_over_p (s : {tfps K m}) :
-  s \in (@coef0_is_1 K m) ->
-  s = exp (prim_tfps ((s^`()%tfps) / (Tfpsp m' s)))%tfps.
+  s \in coef0_eq1 ->
+  s = exp (prim_tfps ((s^`()%tfps) / (trXnt m' s)))%tfps.
 Proof.
 move => s0_eq1; apply: log_inj => //.
-  by rewrite coef0_is_1E coef0_exp // coef0_is_0E coef0_prim_tfps.
-rewrite cancel_log_exp // ?coef0_is_0E ?coef0_prim_tfps //.
-apply: pw_eq => //; last first.
-  by exists 0; rewrite !horner_coef0 coef0_log // coef0_prim_tfps.
-by rewrite deriv_log // prim_tfpsK.
+  by rewrite coef0_eq1E coef0_exp // coef0_eq0E coef0_prim_tfps.
+rewrite expK // ?coef0_eq0E ?coef0_prim_tfps //.
+apply: deriv_tfps_eq => //.
+  by rewrite deriv_log // prim_tfpsK.
+by rewrite coef0_log // coef0_prim_tfps.
 Qed.
 
 Definition newton_inv (p : {tfps K m}) : {poly K} := 
-  revp (exp (prim_tfps (divfX ((p`_0)%:S - p)))).
+  revp (tfps (exp (prim_tfps (divfX ((p`_0)%:S - p))))).
 
 Lemma newton_tfpsK (p : {poly K}) :
   size p <= m.+1 ->  ~~ (root p 0) -> p \is monic ->
@@ -814,21 +807,19 @@ Proof.
 move => sp_lt_Sm Nrootp0 p_monic; rewrite /newton_inv.
 apply: (canLR_in (@revp_involutive _)).
   by rewrite qualifE -horner_coef0.
-have -> : revp p = Tfpsp m (revp p).
-  apply: val_inj => /=; rewrite modp_small //= size_polyXn ltnS.
+have -> : revp p = tfps (Tfpsp m (revp p)).
+  rewrite trXnK //.
   by rewrite (leq_trans (size_revp_leq _)).
 rewrite [Tfpsp _ _ in RHS]exp_prim_derivp_over_p; last first.
-  by rewrite coef0_is_1E nth0_Tfpsp coef0_revp -monicE.
-congr (exp (prim_tfps _)).
+  by rewrite coef0_eq1E coef0_trXn coef0_revp -monicE.
+congr (tfps (exp (prim_tfps _))).
 rewrite (newton_tfps_coef0 f) // -aux_conversion4 //=.
-rewrite modp_small; last first.
-  by rewrite size_polyXn size_revp (leq_ltn_trans (leq_subr _ _)).
 rewrite Tfpsfp_frac; last first.
   by rewrite coef0_revp; move/monicP : p_monic ->; apply: oner_neq0.
-congr (_ / _).
-rewrite deriv_tfpsE /= modp_small // size_polyXn size_revp.
-by rewrite (leq_ltn_trans (leq_subr _ _)).
+rewrite /m; congr (_ / _).
+  by apply tfps_inj; rewrite -deriv_trXn val_deriv_tfps.
+by rewrite trXntE trXn_trXn.
 Qed.
 
 End MoreConversion.
- 
\ No newline at end of file
+
diff --git a/truncpowerseries.v b/truncpowerseries.v
index 7c60219..0a55962 100644
--- a/truncpowerseries.v
+++ b/truncpowerseries.v
@@ -1,15 +1,26 @@
-(* (c) Copyright Microsoft Corporation and Inria. All rights reserved. *)
-
-(*****************************************************************************)
-(*  some doc here                                                            *)
-(*****************************************************************************)
+(** Truncated polynomial, i.e. polynom mod X^n *)
+(******************************************************************************)
+(*       Copyright (C) 2019 Florent Hivert <florent.hivert@lri.fr>            *)
+(*                                                                            *)
+(*  Distributed under the terms of the GNU General Public License (GPL)       *)
+(*                                                                            *)
+(*    This code is distributed in the hope that it will be useful,            *)
+(*    but WITHOUT ANY WARRANTY; without even the implied warranty of          *)
+(*    MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU       *)
+(*    General Public License for more details.                                *)
+(*                                                                            *)
+(*  The full text of the GPL is available at:                                 *)
+(*                                                                            *)
+(*                  http://www.gnu.org/licenses/                              *)
+(******************************************************************************)
 From mathcomp Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq choice.
 From mathcomp Require Import fintype div tuple finfun bigop finset fingroup.
 From mathcomp Require Import perm ssralg poly polydiv mxpoly binomial bigop.
 From mathcomp Require Import finalg zmodp matrix mxalgebra polyXY ring_quotient.
-From Newtonsums Require Import auxresults fraction polyorder polydec revpoly.
+From mathcomp Require Import generic_quotient.
+
+Require Import auxresults.
 
-Import FracField.
 
 Set Implicit Arguments.
 Unset Strict Implicit.
@@ -17,30 +28,135 @@ Unset Printing Implicit Defensive.
 
 Import GRing.Theory.
 Local Open Scope ring_scope.
-Local Open Scope quotient_scope.
 
+Declare Scope tfps_scope.
 Delimit Scope tfps_scope with tfps.
 
-Reserved Notation "{ 'tfps' K n }"
-         (at level 0, K at next level, format "{ 'tfps'  K  n }").
+Reserved Notation "{ 'tfps' R n }"
+         (at level 0, R, n at level 2, format "{ 'tfps'  R  n }").
 Reserved Notation "[ 'tfps' s <= n => F ]"
   (at level 0, n at next level, s ident, format "[ 'tfps' s <= n  =>  F ]").
 Reserved Notation "[ 'tfps' s => F ]"
   (at level 0, s ident, format "[ 'tfps'  s  =>  F ]").
-Reserved Notation "c %:S" (at level 2).
+Reserved Notation "c %:S" (at level 2, format "c %:S").
+Reserved Notation "\X" (at level 0).
+Reserved Notation "\Xo( n )" (at level 0).
 Reserved Notation "f *h g" (at level 2).
-Reserved Notation "f ^` ()" (at level 8).
+Reserved Notation "x ^^ n" (at level 29, left associativity).
+Reserved Notation "f \So g" (at level 50).
+Reserved Notation "\sqrt f" (at level 10).
+
+
+Section SSRCompl.
+
+Variable R : ringType.
+Implicit Type (x y z : R).
+
+Lemma expr_prod i x : x ^+ i = \prod_(j < i) x.
+Proof.
+elim: i => [|i IHi]; first by rewrite expr0 big_ord0.
+by rewrite big_ord_recl -IHi exprS.
+Qed.
+
+Lemma commrB x y z : GRing.comm x y -> GRing.comm x z -> GRing.comm x (y - z).
+Proof. by move=> com_xy com_xz; apply commrD => //; apply commrN. Qed.
+
+Lemma commr_sum (I : Type) (s : seq I) (P : pred I) (F : I -> R) x :
+  (forall i, P i -> GRing.comm x (F i)) -> GRing.comm x (\sum_(i <- s | P i) F i).
+Proof.
+move=> H; rewrite /GRing.comm mulr_suml mulr_sumr.
+by apply eq_bigr => i /H.
+Qed.
+
+End SSRCompl.
+
+Section MoreBigop.
+
+Definition swap (R : Type) (x : R * R) := (x.2, x.1).
+
+Lemma swap_inj (R : Type) : involutive (@swap R).
+Proof. by move => [x1 x2]. Qed.
+
+Variables (R : Type).
+
+Lemma triangular_swap (idx : R) (op : Monoid.com_law idx)
+      (m : nat) (P : 'I_m -> 'I_m -> bool) (F : nat -> nat -> R) :
+  \big[op/idx]_(i < m) \big[op/idx]_(j < m | P i j) F i j =
+  \big[op/idx]_(j < m) \big[op/idx]_(i < m | P i j) F i j.
+Proof. by rewrite !pair_big_dep (reindex_inj (inv_inj (@swap_inj _))). Qed.
+
+Variable (idx : R) (op : Monoid.com_law idx).
+
+Lemma index_translation (m j : nat) (F : nat -> R) :
+  \big[op/idx]_(i < m - j) F i =
+  \big[op/idx]_(k < m | j <= k)  F (k - j)%N.
+Proof.
+rewrite -(big_mkord predT F) /= (big_mknat _ j m (fun k => F (k - j)%N)).
+rewrite -{2}[j]add0n (big_addn 0 m j _ _).
+by apply: eq_bigr => i _ ; rewrite addnK.
+Qed.
+
+Lemma aux_triangular_index_bigop (m : nat) (F : nat -> nat -> R) :
+  \big[op/idx]_(i < m) \big[op/idx]_(j < m | i + j < m) F i j =
+  \big[op/idx]_(k < m) \big[op/idx]_(l < k.+1) F l (k - l)%N.
+Proof.
+evar (G : 'I_m -> R) ; rewrite [LHS](eq_bigr G) => [|i _] ; last first.
+- rewrite (eq_bigl (fun j => nat_of_ord j < (m - (nat_of_ord i))%N))=> [|j /=].
+  + rewrite big_ord_narrow => [ | _ /= ] ; first exact: leq_subr.
+    by rewrite index_translation; symmetry; rewrite /G; reflexivity.
+  + by rewrite ltn_subRL.
+- rewrite /G (triangular_swap _ (fun i k => (nat_of_ord i) <= (nat_of_ord k))
+                                (fun i k => F i (k - i)%N)).
+  apply: eq_big => [ // | i _].
+  rewrite (eq_bigl (fun i0 => (nat_of_ord i0) < i.+1)) => [ | j ] ; last first.
+  + by rewrite -ltnS.
+  + by rewrite big_ord_narrow.
+Qed.
+
+Lemma triangular_index_bigop (m n: nat) (F : nat -> nat -> R) :
+  n <= m ->
+  \big[op/idx]_(i < m) \big[op/idx]_(j < m | i + j < n) F i j =
+  \big[op/idx]_(k < n) \big[op/idx]_(l < k.+1) F l (k - l)%N.
+Proof.
+move => leq_nm.
+rewrite -(subnKC leq_nm) big_split_ord /=.
+rewrite [X in op _ X]big1_seq => [|i _]; last first.
+  rewrite big_hasC // ; apply/hasPn => x _.
+  by rewrite -[X in _ < X]addn0 -addnA ltn_add2l ltn0.
+rewrite Monoid.Theory.simpm /= -aux_triangular_index_bigop.
+apply: eq_bigr => i _ ; rewrite subnKC //.
+rewrite (eq_bigl (fun j => (i + (nat_of_ord j) < n) && ((nat_of_ord j) < n)))
+                                                                    ; last first.
+  move => j; symmetry.
+  rewrite andb_idr //; apply: contraLR; rewrite -!leqNgt => leq_nj.
+  by rewrite (leq_trans leq_nj) // leq_addl.
+by rewrite big_ord_narrow_cond.
+Qed.
+
+End MoreBigop.
 
-Local Notation "p ^ f" := (map_poly f p).
 
 Section MorePolyTheory.
 
-Variable (R : ringType).
+Variable R : ringType.
+Implicit Type p q : {poly R}.
+
+Lemma poly_cat p n :
+  Poly (take n p) + 'X^n * Poly (drop n p) = p.
+Proof.
+apply/polyP=> i; rewrite coefD coefXnM !coef_Poly; case: ltnP => Hi.
+by rewrite nth_take // addr0.
+rewrite nth_drop subnKC // [(take _ _)`_i]nth_default ?add0r //.
+by rewrite size_take -/(minn _ _) (leq_trans (geq_minl _ _) Hi).
+Qed.
 
-Lemma leq_size_deriv (p : {poly R}) : size p^`() <= (size p).-1.
+Fact coef0M p q : (p * q)`_0 = p`_0 * q`_0.
+Proof. by rewrite coefM big_ord_recl big_ord0 addr0. Qed.
+
+Lemma leq_size_deriv (p : {poly R}) : (size p^`() <= (size p).-1)%N.
 Proof.
 have [->|pN0] := eqVneq p 0; first by rewrite deriv0 size_poly0.
-by rewrite -ltnS prednK // ?lt_size_deriv // size_poly_gt0. 
+by rewrite -ltnS prednK // ?lt_size_deriv // size_poly_gt0.
 Qed.
 
 Lemma p_neq0 (p : {poly R}): (exists (x : R), p.[x] != 0) -> p != 0.
@@ -48,13 +164,13 @@ Proof.
 by move => [x px_neq0]; move: px_neq0; apply: contra => /eqP ->; rewrite horner0.
 Qed.
 
-Variable (K : fieldType).
+Variable (K : idomainType).
 
 Fact polyXP (p : {poly K}) : reflect (p`_0 = 0) ('X %| p).
 Proof. by rewrite -['X]subr0 -polyC0 -horner_coef0; apply: polyXsubCP. Qed.
 
-Fact nth0_eq_nth0 (p q : {poly K}) : 
-   p %= q -> (p`_0 == 0) = (q`_0 == 0).
+Fact coef0_eq_coef0 (p q : {poly K}) :
+  p %= q -> (p`_0 == 0) = (q`_0 == 0).
 Proof.
 move => p_eqp_q; rewrite -!horner_coef0.
 apply/(sameP eqP).
@@ -66,7 +182,7 @@ Qed.
 
 Hypothesis char_K_is_zero : [char K] =i pred0.
 
-Fact size_deriv (p : {poly K}) : size (p ^`()%R) = (size p).-1.
+Fact size_deriv (p : {poly K}) : size (p^`()%R) = (size p).-1.
 Proof.
 have [lt_sp_1 | le_sp_1] := ltnP (size p) 2.
   move: (size1_polyC lt_sp_1) => ->.
@@ -83,1557 +199,2995 @@ move: (ltn_predK le_sp_1) => H.
 by move: le_sp_1 ; rewrite -{1}H -[X in _ < X]add1n -add1n leq_add2l.
 Qed.
 
-Lemma p_cst (p : {poly K}) : p ^`() = 0 -> {c : K | p = c %:P}.
+Lemma deriv_eq0 (p : {poly K}) : p^`() = 0 -> {c : K | p = c %:P}.
 Proof.
 move/eqP ; rewrite -size_poly_eq0 size_deriv.
 move/eqP => H_size_p.
 exists p`_0 ; apply: size1_polyC.
-by rewrite (leq_trans (leqSpred _)) // H_size_p. 
+by rewrite (leq_trans (leqSpred _)) // H_size_p.
 Qed.
 
-(* this kind of injectivity + deriv result could be useful ? *)
-(* Lemma deriv_poly_eq (K : fieldType) (p q : {poly K}) : 
-    p`_0 == q`_0 -> p^`() == q^`() -> p = q.
-Proof.
-rewrite -subr_eq0 -coefB -[p^`() == q^`()]subr_eq0 -derivB.
-move => coef0_eq0 deriv_eq0 ; apply/eqP.
-rewrite -subr_eq0 ; apply/eqP ; move: coef0_eq0 deriv_eq0.
-exact: deriv_poly_eq0.
-Qed. *)
-
 End MorePolyTheory.
 
-Section ModPolyTheory.
 
-Variable (K : fieldType).
+Section TruncFPSDef.
 
-Fact leq_modpXn m (p : {poly K}) : size (p %% 'X^m) <= m.
-Proof.
-by rewrite -ltnS (leq_trans (ltn_modpN0 _ _)) // -?size_poly_eq0 size_polyXn.
-Qed.
+Variable R : ringType.
+Variable n : nat.
 
-Lemma coef_modXn m (p : {poly K}) i : (p %% 'X^m)`_i =
-  if i < m then p`_i else 0.
-Proof.
-have [lt_i_m|le_m_i] := ltnP; last first.
-  by rewrite nth_default // (leq_trans (leq_modpXn _ _)).
-have /polyP /(_ i) := divp_eq p 'X^m.
-by rewrite coefD coefMXn lt_i_m add0r.
-Qed.
+Implicit Types (p q r s : {poly R}).
 
-(* should not be visible outside this file *)
-Fact modCXn a n : 0 < n -> a%:P %% 'X^n = a%:P :> {poly K}.
-Proof. 
-move=> lt_0n. 
-by rewrite modp_small // size_polyC size_polyXn (leq_ltn_trans (leq_b1 _)).
-Qed.
+Record truncfps := MkTfps { tfps : {poly R}; _ : size tfps <= n.+1 }.
+
+Canonical truncfps_subType :=
+  Eval hnf in [subType for tfps].
+Definition truncfps_eqMixin :=
+  Eval hnf in [eqMixin of truncfps by <:].
+Canonical truncfps_eqType :=
+  Eval hnf in EqType truncfps truncfps_eqMixin.
+Definition truncfps_choiceMixin :=
+  [choiceMixin of truncfps by <:].
+Canonical truncfps_choiceType :=
+  Eval hnf in ChoiceType truncfps truncfps_choiceMixin.
+
+Lemma tfps_inj : injective tfps. Proof. exact: val_inj. Qed.
+
+Definition tfps_of of phant R := truncfps.
+Identity Coercion type_tfps_of : tfps_of >-> truncfps.
+
+Fact poly_of_tfps_key : unit. Proof. by []. Qed.
+Definition poly_of_tfps : tfps_of (Phant R) -> {poly R} :=
+  locked_with poly_of_tfps_key tfps.
+Canonical poly_of_tfps_unlockable := [unlockable fun poly_of_tfps].
+
+Lemma tfpsE : tfps =1 poly_of_tfps.
+Proof. by case=> p Hp; rewrite unlock. Qed.
+
+Coercion seq_of_tfps (f : truncfps) : seq R := @tfps f.
+
+Lemma size_tfps (f : tfps_of (Phant R)) : size f <= n.+1.
+Proof. by case: f. Qed.
+
+Definition coeftfps_head h i (p : tfps_of (Phant R)) := let: tt := h in p`_i.
+
+End TruncFPSDef.
+
+(* We need to break off the section here to let the Bind Scope directives     *)
+(* take effect.                                                               *)
+Bind Scope ring_scope with tfps_of.
+Bind Scope ring_scope with truncfps.
+Arguments tfps {R n%N}.
+Arguments tfps_inj {R} [p1%R p2%R] : rename.
+Notation "{ 'tfps' R n }" :=  (tfps_of n (Phant R)).
+Arguments coeftfps_head {R n} h i%N p%R.
+Notation coeftfps i := (coeftfps_head tt i).
+
+Hint Resolve size_tfps : core.
+
+
+Section CoefTFPS.
+
+Variable R : ringType.
+Variable n : nat.
+
+Implicit Types (p q r s : {poly R}) (f g : {tfps R n}).
+
+Lemma size_tfpsE f : size f = size (tfps f).
+Proof. by []. Qed.
+
+Lemma coef_tfpsE f i : f`_i = (tfps f)`_i.
+Proof. by []. Qed.
 
-Fact modp_modp (p u v : {poly K}) : u %| v -> (p %% v) %% u = p %% u.
+Lemma coef_tfps f i : f`_i = if i <= n then f`_i else 0.
 Proof.
-move => dvdp_u_v.
-have [->|v_neq0] := eqVneq v 0; first by rewrite modp0.
-rewrite (divp_eq p v) modp_addl_mul_small ?ltn_modp //.
-by rewrite modp_add [X in X + _]modp_eq0 ?dvdp_mull // add0r.
+case: (leqP i n) => Hi //.
+by rewrite nth_default // (leq_trans (size_tfps _) Hi).
 Qed.
 
-Fact coef0M (p q : {poly K}) : (p * q)`_0 = p`_0 * q`_0.
-(* Proof. by rewrite coefM big_ord_recl big_ord0 addr0. Qed. *)
-Proof. by rewrite -!horner_coef0 hornerM. Qed.
-
-(* should not be visible outside this file *)
-Fact modX_eq0 (p : {poly K}) (n m : nat) : p`_0 = 0 -> n < m ->
-  (p ^+ m) %% 'X^n.+1 = 0.
+Lemma tfpsP f g : (forall i, i <= n -> f`_i = g`_i) <-> (f = g).
 Proof.
-rewrite -horner_coef0 => /polyXsubCP p0_eq0 n_lt_m.
-rewrite polyC0 subr0 in p0_eq0.
-apply/modp_eq0P.
-by rewrite (dvdp_trans (dvdp_exp2l ('X : {poly K}) n_lt_m)) // dvdp_exp2r.
+split => [H | H i Hi].
+- apply/tfps_inj/polyP => i; rewrite [LHS]coef_tfps [RHS]coef_tfps.
+  by case: leqP => //; apply: H.
+- move: H => /(congr1 tfps)/(congr1 (fun r => r`_i)).
+  by rewrite coef_tfps Hi.
 Qed.
 
-End ModPolyTheory.
 
-Section MoreBigop.
+Definition Tfps_of (p : {poly R}) (p_small : size p <= n.+1)
+  : {tfps R n} := MkTfps p_small.
 
-Definition swap (R : Type) (x : R * R) := (x.2, x.1).
+Fact trXn_subproof p : size (Poly (take n.+1 p)) <= n.+1.
+Proof. by apply: (leq_trans (size_Poly _)); rewrite size_take geq_minl. Qed.
+Definition trXn_def p := Tfps_of (trXn_subproof p).
+Fact trXn_key : unit. Proof. by []. Qed.
+Definition trXn := locked_with trXn_key trXn_def.
+Canonical trXn_unlockable := [unlockable fun trXn].
 
-Lemma swap_inj (R : Type) : involutive (@swap R).
-Proof. by move => [x1 x2]. Qed.
+Definition tfpsC_def c := trXn (c %:P).
+Fact tfpsC_key : unit. Proof. by []. Qed.
+Definition tfpsC := locked_with tfpsC_key tfpsC_def.
+Canonical tfpsC_unlockable := [unlockable fun tfpsC].
 
-Lemma triangular_swap (R : Type) (idx : R) (op : Monoid.com_law idx)
-                 (m : nat) (P : 'I_m -> 'I_m -> bool) (F : nat -> nat -> R) :
-  \big[op/idx]_(i < m) \big[op/idx]_(j < m | P i j) F i j =
-  \big[op/idx]_(j < m) \big[op/idx]_(i < m | P i j) F i j.
-Proof. by rewrite !pair_big_dep (reindex_inj (inv_inj (@swap_inj _))). Qed.
+Definition tfps_of_fun (f : nat -> R) := Tfps_of (size_poly _ f).
 
-Lemma index_translation (R : Type) (idx : R) (op : Monoid.law idx)
-                                                     (m j : nat) (F : nat -> R) :
-  \big[op/idx]_(i < m - j) F i =
-  \big[op/idx]_(k < m | j <= k)  F (k - j)%N.
+Lemma trXnE p : tfps (trXn p) = Poly (take n.+1 p) :> {poly R}.
+Proof. by rewrite unlock. Qed.
+
+Lemma coef_trXn p i : (trXn p)`_i = if i <= n then p`_i else 0.
 Proof.
-rewrite -(big_mkord predT F) /= (big_mknat _ j m (fun k => F (k - j)%N)).
-rewrite -{2}[j]add0n (big_addn 0 m j _ _).
-by apply: eq_bigr => i _ ; rewrite addnK.
+rewrite coef_tfpsE trXnE coef_Poly.
+case: leqP => Hi; first by rewrite nth_take.
+by rewrite nth_default // size_take -/(minn _ _) (leq_trans (geq_minl _ _) Hi).
 Qed.
 
-Lemma aux_triangular_index_bigop (R : Type) (idx : R) (op : Monoid.com_law idx)
-                                                (m : nat) (F : nat -> nat -> R) :
-  \big[op/idx]_(i < m) \big[op/idx]_(j < m | i + j < m) F i j =
-  \big[op/idx]_(k < m) \big[op/idx]_(l < k.+1) F l (k - l)%N.
+Lemma trXnP p q : (forall i, i <= n -> p`_i = q`_i) <-> (trXn p = trXn q).
 Proof.
-evar (G : 'I_m -> R) ; rewrite [LHS](eq_bigr G) => [|i _] ; last first.
-+ rewrite (eq_bigl (fun j => nat_of_ord j < (m - (nat_of_ord i))%N))=> [|j /=].
-- rewrite big_ord_narrow => [ | _ /= ] ; first exact: leq_subr.
-  by rewrite index_translation; symmetry; rewrite /G; reflexivity.
-- by rewrite ltn_subRL.
-+ rewrite /G (triangular_swap _ (fun i k => (nat_of_ord i) <= (nat_of_ord k))
-                                (fun i k => F i (k - i)%N)).
-  apply: eq_big => [ // | i _].
-  rewrite (eq_bigl (fun i0 => (nat_of_ord i0) < i.+1)) => [ | j ] ; last first.
-- by rewrite -ltnS.
-- by rewrite big_ord_narrow.
+rewrite -tfpsP; split => H i Hi.
+- by rewrite !coef_trXn Hi; apply H.
+- by have := H i Hi; rewrite !coef_trXn Hi.
 Qed.
 
-Lemma triangular_index_bigop (R : Type) (idx : R) (op : Monoid.com_law idx)
-                             (m n: nat) (F : nat -> nat -> R) :
-  n <= m ->
-  \big[op/idx]_(i < m) \big[op/idx]_(j < m | i + j < n) F i j =
-  \big[op/idx]_(k < n) \big[op/idx]_(l < k.+1) F l (k - l)%N.
+Lemma tfpsK : cancel (@tfps R n) trXn.
+Proof. by move=> f; apply/tfpsP => i Hi; rewrite coef_trXn Hi. Qed.
+
+Lemma trXnK p : size p <= n.+1 -> tfps (trXn p) = p.
 Proof.
-move => leq_nm.
-rewrite -(subnKC leq_nm) big_split_ord /=.
-rewrite [X in op _ X]big1_seq => [|i _]; last first.
-  rewrite big_hasC // ; apply/hasPn => x _.
-  by rewrite -[X in _ < X]addn0 -addnA ltn_add2l ltn0.
-rewrite Monoid.Theory.simpm /= -aux_triangular_index_bigop.
-apply: eq_bigr => i _ ; rewrite subnKC //.
-rewrite (eq_bigl (fun j => (i + (nat_of_ord j) < n) && ((nat_of_ord j) < n)))
-                                                                    ; last first.
-  move => j; symmetry.
-  rewrite andb_idr //; apply: contraLR; rewrite -!leqNgt => leq_nj.
-  by rewrite (leq_trans leq_nj) // leq_addl.
-by rewrite big_ord_narrow_cond.
+move=> le_szn; apply polyP => i.
+rewrite -coef_tfpsE coef_trXn; case: leqP => // /(leq_trans le_szn) leq_szi.
+by rewrite nth_default.
 Qed.
 
-End MoreBigop.
+Lemma coef0_trXn (p : {poly R}) : (trXn p)`_0 = p`_0.
+Proof. by rewrite coef_trXn leq0n. Qed.
+
+
+Lemma tfpsCE c : tfpsC c = trXn c%:P.
+Proof. by rewrite unlock. Qed.
 
-Section TruncatedPowerSeries.
+Lemma coef_tfpsC c i : (tfpsC c)`_i = if i == 0%N then c else 0.
+Proof.
+by rewrite tfpsCE coef_trXn coefC; case: i => //= i; rewrite if_same.
+Qed.
 
-Variables (K : fieldType) (n : nat).
+Lemma val_tfpsC (c : R) : tfps (tfpsC c) = c %:P.
+Proof. by apply/polyP => i /=; rewrite coef_tfpsC coefC. Qed.
 
-Record tfps := MkTfps
-{
-  truncated_tfps :> {poly K};
-  _ : size truncated_tfps <= n.+1
-}.
+Lemma tfpsCK : cancel tfpsC (coeftfps 0).
+Proof. by move=> c; rewrite [coeftfps 0 _]coef_tfpsC. Qed.
 
-Definition tfps_of of phant K := tfps.
-Local Notation "'{tfps}'" := (tfps_of (Phant K)).
 
-Canonical tfps_subType := [subType for truncated_tfps].
-Definition tfps_eqMixin := [eqMixin of tfps by <:].
-Canonical tfps_eqType := EqType {tfps} tfps_eqMixin.
-Definition tfps_choiceMixin := [choiceMixin of tfps by <:].
-Canonical tfps_choiceType := ChoiceType {tfps} tfps_choiceMixin.
+Lemma tfpsC_inj : injective tfpsC.
+Proof.
+by move=> c1 c2 eqc12; have:= coef_tfpsC c2 0; rewrite -eqc12 coef_tfpsC.
+Qed.
+
 
-Definition Tfps_of (p : {poly K}) (p_small : size p <= n.+1) : 
-    {tfps} := MkTfps p_small.
+Lemma coef_tfps_of_fun (f : nat -> R) i :
+  (tfps_of_fun f)`_i = if i <= n then f i else 0.
+Proof. by rewrite /tfps_of_fun coef_poly ltnS. Qed.
 
-Definition Tfpsp (p : {poly K}) := Tfps_of (leq_modpXn _ p).
 
-Definition tfps_of_fun (f : nat -> K) := Tfps_of (size_poly _ f).
+Definition poly_trXn_class := QuotClass tfpsK.
+Canonical poly_trXn_type := QuotType {tfps R n} poly_trXn_class.
 
-End TruncatedPowerSeries.
+Lemma poly_trXn_quotP p q :
+  reflect
+    (forall i, (i <= n)%N -> p`_i = q`_i)
+    (p == q %[mod {tfps R n}])%qT.
+Proof. by rewrite !unlock /pi_phant; apply (iffP eqP); rewrite trXnP. Qed.
 
-Section TruncatedPowerSeriesTheory.
+End CoefTFPS.
 
-Variables (K : fieldType) (n : nat).
+Local Open Scope tfps_scope.
 
-Local Notation "{ 'tfps' K n }" := (tfps_of n (Phant K)).
-Local Notation tfps := {tfps K n}.
-Local Notation "[ 'tfps' s <= n => F ]" := (tfps_of_fun n (fun s => F)).
-Local Notation "[ 'tfps' s => F ]" := [tfps s <= n => F].
+Notation "[ 'tfps' s <= n => F ]" :=
+  (tfps_of_fun n (fun s => F)) : tfps_scope.
+Notation "[ 'tfps' s => F ]" := [tfps s <= _ => F] : tfps_scope.
+Notation "c %:S" := (tfpsC _ c) (at level 2) : tfps_scope.
+Notation "\X" := (trXn _ 'X) : tfps_scope.
+Notation "\Xo( n )" := (trXn n 'X) (only parsing): tfps_scope.
 
-Implicit Types (f g : tfps).
 
-Lemma size_tfps f : size (val f) <= n.+1.
-Proof. by case: f. Qed.
+Section TFPSTheory.
 
-Fact mod_tfps (m : nat) f : n <= m -> f %% 'X^m.+1 = (val f).
+Variable (R : ringType).
+Implicit Types (p q r s : {poly R}).
+
+Fact trXnC n a : tfps (trXn n a%:P) = a%:P :> {poly R}.
 Proof.
-move => leq_nm.
-by rewrite modp_small // size_polyXn ltnS (leq_trans (size_tfps _)).
+apply/polyP => i; rewrite coef_trXn coefC.
+by case: eqP => [->|_] //; rewrite if_same.
 Qed.
 
-Fact Tfpsp_modp (m : nat) (p : {poly K}) : n < m ->
-    Tfpsp n (p %% 'X^m) = Tfpsp n p.
-Proof. by move=> lt_nm; apply/val_inj=> /=; rewrite modp_modp // dvdp_exp2l. Qed.
+Fact trXn_trXn p m n : m <= n -> trXn m (tfps (trXn n p)) = trXn m p.
+Proof.
+move=> le_mn; apply/trXnP => i le_im.
+by rewrite coef_trXn (leq_trans le_im le_mn).
+Qed.
 
-Lemma tfps_nth_default f j : j > n ->  f`_j = 0.
-Proof. by move=> j_big; rewrite nth_default // (leq_trans _ j_big) ?size_tfps. Qed.
+Variable (n : nat).
 
-Lemma tfps_coefK f : [tfps s => f`_s] = f.
+Lemma trXnCE m a : trXn n (tfps (a%:S : {tfps R m})) = a%:S.
+Proof. by apply tfps_inj; rewrite val_tfpsC !tfpsCE. Qed.
+
+Lemma trXn_mull p q : trXn n (tfps (trXn n p) * q) = trXn n (p * q).
 Proof.
-apply/val_inj/polyP=> j; rewrite coef_poly ltnS.
-by have  [//|j_big] := leqP; rewrite tfps_nth_default.
+apply/trXnP => i le_in /=; rewrite !coefM.
+apply eq_bigr => [] [j] /=; rewrite ltnS => le_ji _.
+by rewrite coef_trXn (leq_trans le_ji le_in).
 Qed.
 
-Lemma coef_tfps s (f : nat -> K) :
-  [tfps s => f s]`_s = if s <= n then f s else 0.
-Proof. by rewrite coef_poly. Qed.
-
-Lemma eq_tfps f g : (forall i : 'I_n.+1, f`_i = g`_i) <-> (f = g).
+Lemma trXn_mulr p q : trXn n (p * tfps (trXn n q)) = trXn n (p * q).
 Proof.
-split=> [eq_s|-> //]; apply/val_inj/polyP => i /=.
-have [i_small|i_big] := ltnP i n.+1; first by rewrite (eq_s (Ordinal i_small)).
-by rewrite -[f]tfps_coefK -[g]tfps_coefK !coef_tfps leqNgt i_big.
+apply/trXnP => i le_in /=; rewrite !coefM.
+apply eq_bigr => [] [j] /=; rewrite ltnS => le_ji _.
+by rewrite coef_trXn (leq_trans (leq_subr _ _) le_in).
 Qed.
 
-Lemma nth0_Tfpsp (p : {poly K}) : (Tfpsp n p)`_0 = p`_0.
-Proof. by rewrite coef_modXn ltn0Sn. Qed.
+Lemma trXn_mul p q :
+  trXn n (tfps (trXn n p) * tfps (trXn n q)) = trXn n (p * q).
+Proof. by rewrite trXn_mulr trXn_mull. Qed.
+
 
 (* zmodType structure *)
+Implicit Types (f g : {tfps R n}).
 
-Fact zero_tfps_subproof : size (0 : {poly K}) <= n.+1.
+Fact zero_tfps_subproof : size (0 : {poly R}) <= n.+1.
 Proof. by rewrite size_poly0. Qed.
-
 Definition zero_tfps := Tfps_of zero_tfps_subproof.
 
 Lemma add_tfps_subproof f g :
-  size (val f + val g) <= n.+1.
+  size (tfps f + tfps g) <= n.+1.
 Proof. by rewrite (leq_trans (size_add _ _)) // geq_max !size_tfps. Qed.
-
 Definition add_tfps f g := Tfps_of (add_tfps_subproof f g).
 
-Lemma opp_tfps_proof f : size (- val f) <= n.+1.
+Lemma opp_tfps_subproof f : size (- tfps f) <= n.+1.
 Proof. by rewrite size_opp ?size_tfps. Qed.
+Definition opp_tfps f := Tfps_of (opp_tfps_subproof f).
+
+Program Definition tfps_zmodMixin :=
+  @ZmodMixin {tfps R n} zero_tfps opp_tfps add_tfps _ _ _ _.
+Next Obligation. by move => f1 f2 f3; apply/tfps_inj/addrA. Qed.
+Next Obligation. by move => f1 f2; apply/tfps_inj/addrC. Qed.
+Next Obligation. by move => f; apply/tfps_inj/add0r. Qed.
+Next Obligation. by move => f; apply/tfps_inj/addNr. Qed.
+Canonical tfps_zmodType := ZmodType {tfps R n} tfps_zmodMixin.
 
-Definition opp_tfps f := Tfps_of (opp_tfps_proof f).
+Fact trXn_is_additive : additive (trXn n).
+Proof.
+by move=> f g; apply/tfpsP => i Hi; rewrite coefB !coef_trXn coefB Hi.
+Qed.
+Canonical trXn_additive := Additive trXn_is_additive.
 
-Fact add_tfpsA : associative add_tfps.
-Proof. by move => f1 f2 f3; apply/val_inj; apply: addrA. Qed.
+Lemma coef_tfps0 i : (0 : {tfps R n})`_i = 0.
+Proof. by rewrite coef0. Qed.
 
-Fact add_tfpsC : commutative add_tfps.
-Proof. by move => f1 f2; apply/val_inj; apply: addrC. Qed.
+Lemma trXn0 : trXn n 0 = 0.
+Proof. exact: raddf0. Qed.
 
-Fact add_tfps0f : left_id zero_tfps add_tfps.
-Proof. by move => f; apply/val_inj; apply: add0r. Qed.
+Fact tfps_is_additive : additive (@tfps R n : {tfps R n} -> {poly R}).
+Proof. by []. Qed.
+Canonical tfps_additive := Additive tfps_is_additive.
 
-Fact add_tfpsK : left_inverse zero_tfps opp_tfps add_tfps.
-Proof. by move => f; apply/val_inj; apply: addNr. Qed.
+Lemma tfpsC_is_additive : additive (@tfpsC R n : R -> {tfps R n}).
+Proof.
+move=> c1 c2; apply tfps_inj.
+by rewrite !val_tfpsC !raddfB /= !val_tfpsC.
+Qed.
+Canonical tfpsC_additive := Additive tfpsC_is_additive.
 
-Definition tfps_zmodMixin :=
-                              ZmodMixin add_tfpsA add_tfpsC add_tfps0f add_tfpsK.
-Canonical tfps_zmodType := ZmodType tfps tfps_zmodMixin.
+Lemma tfpsC0 : (0%:S : {tfps R n}) = 0.
+Proof. exact: raddf0. Qed.
 
-Lemma Tfpsp0 : Tfpsp n 0 = 0.
-Proof. by apply/val_inj => /=; rewrite mod0p. Qed.
 
 (* ringType structure *)
-
-Fact one_tfps_proof : size (1 : {poly K}) <= n.+1.
+Fact one_tfps_proof : size (1 : {poly R}) <= n.+1.
 Proof. by rewrite size_polyC (leq_trans (leq_b1 _)). Qed.
+Definition one_tfps : {tfps R n} := Tfps_of one_tfps_proof.
 
-Definition one_tfps : tfps := Tfps_of one_tfps_proof.
-
-Definition mul_tfps f g := Tfpsp n (val f * val g).
-
-Definition hmul_tfps f g := [tfps j => f`_j * g`_j].
-
-Definition deriv_tfps f : {tfps K n.-1} := [tfps s <= n.-1 => f`_s.+1 *+ s.+1]. 
-
+Definition mul_tfps f g := trXn n (tfps f * tfps g).
+Definition hmul_tfps f g := [tfps j <= n => f`_j * g`_j].
 Local Notation "f *h g" := (hmul_tfps f g) (at level 2).
 
-Lemma hmul_tfpsC : commutative hmul_tfps.
-Proof.
-by move=> f1 f2; apply/val_inj/polyP => /= i; rewrite !coef_poly mulrC.
-Qed.
-
 Lemma hmul_tfpsA : associative hmul_tfps.
 Proof.
-move=> f1 f2 f3; apply/val_inj/polyP => /= i.
-by rewrite // !coef_poly; case: (_ < _) => //; apply: mulrA.
+by move=> f1 f2 f3; apply/tfpsP => i Hi; rewrite !coef_poly ltnS Hi mulrA.
 Qed.
 
 Lemma hmul_tfps0r f : 0 *h f = 0.
-Proof.
-by apply/val_inj/polyP=> i /=; rewrite coef_poly coef0 mul0r if_same.
-Qed.
+Proof. by apply/tfpsP => i Hi; rewrite coef_poly coef0 mul0r if_same. Qed.
 
 Lemma hmul_tfpsr0 f : f *h 0 = 0.
-Proof. by rewrite hmul_tfpsC hmul_tfps0r. Qed.
-
-Fact left_id_one_mul_tfps : left_id one_tfps mul_tfps.
-Proof.
-move=> p; apply val_inj; rewrite /= mul1r.
-by rewrite modp_small // size_polyXn ltnS ?size_tfps.
-Qed.
-
-Fact mul_tfpsC : commutative mul_tfps.
-Proof. by move=> f1 f2; apply val_inj => /=; rewrite mulrC. Qed.
-
-Fact left_distributive_mul_tfps : left_distributive mul_tfps add_tfps.
-Proof. by move=> f1 f2 f3; apply val_inj => /=; rewrite mulrDl modp_add. Qed.
+Proof. by apply/tfpsP => i Hi; rewrite coef_poly coef0 mulr0 if_same. Qed.
 
-Fact mul_tfpsA : associative mul_tfps.
-Proof.
-move=> f1 f2 f3; apply/val_inj.
-by rewrite /= [in RHS]mulrC !modp_mul mulrA mulrC.
-Qed.
+Program Definition tfps_ringMixin :=
+  @RingMixin [zmodType of {tfps R n}] one_tfps mul_tfps _ _ _ _ _ _.
+Next Obligation. move=> f1 f2 f3;
+                 by rewrite /mul_tfps trXn_mulr trXn_mull mulrA. Qed.
+Next Obligation. by move=> p; rewrite /mul_tfps mul1r tfpsK. Qed.
+Next Obligation. by move=> p; rewrite /mul_tfps mulr1 tfpsK. Qed.
+Next Obligation. by move=> f1 f2 f3; rewrite /mul_tfps mulrDl raddfD. Qed.
+Next Obligation. by move=> f1 f2 f3; rewrite /mul_tfps mulrDr raddfD. Qed.
+Next Obligation. by rewrite -val_eqE oner_neq0. Qed.
+Canonical tfps_ringType := RingType {tfps R n} tfps_ringMixin.
 
-Fact one_tfps_not_zero : one_tfps != 0.
-Proof. by rewrite -val_eqE oner_neq0. Qed.
 
-Definition tfps_ringMixin := ComRingMixin mul_tfpsA mul_tfpsC
-               left_id_one_mul_tfps left_distributive_mul_tfps one_tfps_not_zero.
+Lemma coef_tfps1 i : (1 : {tfps R n})`_i = (i == 0%N)%:R.
+Proof. by rewrite coef1. Qed.
 
-Canonical tfps_ringType := RingType tfps tfps_ringMixin.
-Canonical tfps_comRingType := ComRingType tfps mul_tfpsC.
+Lemma trXn1 : trXn n 1 = 1.
+Proof. by apply/tfpsP => i Hi; rewrite coef_trXn Hi. Qed.
 
-(* comUnitRingType structure *)
+Fact trXn_is_multiplicative : multiplicative (@trXn R n).
+Proof. by split => [f g|] /=; [rewrite -trXn_mul | rewrite trXn1]. Qed.
+Canonical trXn_multiplicative := AddRMorphism trXn_is_multiplicative.
 
-Lemma coef_Tfpsp (p : {poly K}) s : (Tfpsp n p)`_s = if s <= n then p`_s else 0.
-Proof. by rewrite coef_modXn. Qed.
+Lemma mul_tfps_val f g : f * g = trXn n (tfps f * tfps g).
+Proof. by []. Qed.
 
-Fixpoint coef_inv_rec (p : {poly K}) (m i : nat) : K :=
-  match m with
-    | O => p`_(locked 0%N) ^-1
-    | S m => if i == 0%N then p`_(locked 0%N) ^-1
-             else - p`_(locked 0%N) ^-1 * \sum_(k < i) p`_(i - k)
-                                        * coef_inv_rec p m k
-  end.
+Lemma coefM_tfps f g (i : nat) :
+  (f * g)`_i = if i <= n then \sum_(j < i.+1) f`_j * g`_(i - j) else 0.
+Proof. by rewrite !coef_tfpsE mul_tfps_val coef_trXn coefM. Qed.
 
-Definition coef_inv (p : {poly K}) i : K := coef_inv_rec p i i.
+Lemma coefMr_tfps f g (i : nat) :
+  (f * g)`_i = if i <= n then \sum_(j < i.+1) f`_(i - j) * g`_j else 0.
+Proof. by rewrite !coef_tfpsE mul_tfps_val coef_trXn coefMr. Qed.
 
-Lemma coef_inv_recE (p : {poly K}) m i : i <= m ->
-  coef_inv_rec p m i = coef_inv p i.
+Lemma exp_tfps_val f (m : nat) : f ^+ m = trXn n ((tfps f) ^+ m).
 Proof.
-rewrite /coef_inv; elim: m {-2}m (leqnn m) i=> [k | m IHm].
-  by rewrite leqn0 => /eqP -> i ; rewrite leqn0 => /eqP ->.
-case=> [k i |k];  first by rewrite leqn0 => /eqP ->.
-rewrite ltnS => le_km [ // | i ] ; rewrite ltnS => le_ik /=.
-congr (_ * _) ; apply: eq_bigr => l _.
-by rewrite !IHm 1?(leq_trans (leq_ord _)) // (leq_trans le_ik).
+elim: m => [|m IHm]; first by rewrite !expr0 trXn1.
+by rewrite exprS {}IHm /= !rmorphX /= tfpsK -exprS.
 Qed.
 
-Lemma coef_inv0 (p: {poly K}) : coef_inv p 0 = p`_0 ^-1.
-Proof. by rewrite /coef_inv /= -lock. Qed.
-
-Lemma coef_invS (p: {poly K}) j : coef_inv p j.+1 =
-    -(p`_0 ^-1) * (\sum_(k < j.+1) p`_(j.+1 - k) * (coef_inv p k)).
+Lemma tfpsC_is_multiplicative :
+  multiplicative (@tfpsC R n : R -> {tfps R n}).
 Proof.
-rewrite /coef_inv /= -lock; congr (_ * _) ; apply: eq_bigr => k _.
-by rewrite coef_inv_recE // leq_ord.
+split => [c1 c2|]; last by rewrite tfpsCE trXn1.
+apply tfps_inj; rewrite mul_tfps_val !val_tfpsC -rmorphM /=.
+apply/polyP => i; rewrite coef_tfps coef_trXn coefC; case: i => //= i.
+by rewrite !if_same.
 Qed.
+Canonical tfpsC_rmorphism := AddRMorphism tfpsC_is_multiplicative.
 
-Definition unit_tfps : pred tfps := fun f => (f`_0 \in GRing.unit).
+Lemma tfpsC1 : (1%:S : {tfps R n}) = 1.
+Proof. exact: rmorph1. Qed.
 
-Definition inv_tfps f :=
-    if f \in unit_tfps then [tfps s => coef_inv f s] else f.
+Lemma tfpsCM :
+  {morph (fun x => (x%:S : {tfps R n})) : a b / a * b >-> a * b}.
+Proof. exact: rmorphM. Qed.
 
-Fact coef_inv_tfps_subproof f i : f \in unit_tfps ->
-  (inv_tfps f)`_i =
-  if i > n then 0 else
-  if i == 0%N then f`_0 ^-1 else
-  - (f`_0 ^-1) * (\sum_(j < i) f`_(i - j) * (inv_tfps f)`_j).
-Proof.
-have [i_big|i_small] := ltnP; first by rewrite tfps_nth_default.
-move=> f_unit; rewrite /inv_tfps f_unit !coef_tfps.
-case: i => [|i] in i_small *; first by rewrite coef_inv0.
-rewrite i_small coef_invS.
-congr (_ * _); apply: eq_bigr => j _; rewrite coef_tfps ifT //.
-by rewrite (leq_trans _ i_small) // leqW ?leq_ord.
-Qed. 
 
-Fact nonunit_inv_tfps : {in [predC unit_tfps], inv_tfps =1 id}.
-Proof. by move=> f; rewrite inE /inv_tfps /= => /negPf ->. Qed.
+(* lmodType structure *)
+Lemma scale_tfps_subproof (c : R) f : size (c *: val f) <= n.+1.
+Proof. exact: leq_trans (size_scale_leq _ _) (size_tfps _). Qed.
+Definition scale_tfps (c : R) f := Tfps_of (scale_tfps_subproof c f).
 
-Fact unit_tfpsP f g : g * f = 1 -> unit_tfps f.
-Proof.
-move=> /val_eqP /eqP.
-move/(congr1 (fun x => (val x)`_O)).
-rewrite coef_modXn coef0M coefC eqxx /unit_tfps mulrC => h. 
-by apply/unitrPr; exists g`_0.
-Qed.
+Program Definition tfps_lmodMixin :=
+  @LmodMixin R [zmodType of {tfps R n}] scale_tfps _ _ _ _.
+Next Obligation. by apply/tfpsP => i le_in /=; rewrite !coefZ mulrA. Qed.
+Next Obligation.
+  by move=> x; apply/tfpsP => i le_in; rewrite coef_tfpsE /= scale1r. Qed.
+Next Obligation.
+  by move=> r x y; apply/tfpsP => i; rewrite coef_tfpsE /= scalerDr. Qed.
+Next Obligation.
+  by move=> r s; apply/tfpsP => i; rewrite coef_tfpsE /= scalerDl. Qed.
+Canonical tfps_lmodType :=
+  Eval hnf in LmodType R {tfps R n} tfps_lmodMixin.
 
-Fact tfps_mulVr : {in unit_tfps, left_inverse 1 inv_tfps *%R}.
+Fact trXn_is_linear : linear (@trXn R n).
 Proof.
-move=> f f_unit; apply/val_inj; rewrite /inv_tfps f_unit /=.
-apply/polyP => i; rewrite coef_modXn.
-have [i_small | i_big] := ltnP; last first. 
-  by rewrite coefC gtn_eqF // (leq_trans _ i_big).
-rewrite coefC; case: i => [|i] in i_small *.
-  by rewrite coef0M coef_poly /= coef_inv0 mulVr.
-rewrite coefM big_ord_recr coef_poly i_small subnn.
-apply: canLR (addNKr _) _; rewrite addr0.
-apply: canLR (mulrVK _) _; rewrite // mulrC mulrN -mulNr.
-rewrite coef_invS; congr (_ * _); apply: eq_bigr => j _ /=.
-by rewrite mulrC coef_poly (leq_trans _ i_small) 1?leqW.
+move=> c f g; apply/tfpsP => i Hi.
+by rewrite !(coefD, coefZ, coef_trXn) Hi.
 Qed.
+Canonical trXn_linear := AddLinear trXn_is_linear.
 
-Definition tfps_comUnitRingMixin := ComUnitRingMixin
-  tfps_mulVr unit_tfpsP nonunit_inv_tfps.
-
-Canonical unit_tfpsRingType := UnitRingType tfps tfps_comUnitRingMixin.
-
-Lemma coef_inv_tfps f i : f \is a GRing.unit -> f^-1`_i =
-  if i > n then 0 else
-  if i == 0%N then f`_0 ^-1
-  else - (f`_0 ^-1) * (\sum_(j < i) f`_(i - j) * f^-1`_j).
-Proof. exact: coef_inv_tfps_subproof. Qed.
-
-Fact val_mul_tfps f g : val (f * g) = (val f) * (val g) %% 'X^n.+1.
+Fact tfps_is_linear : linear (@tfps R n : {tfps R n} -> {poly R}).
 Proof. by []. Qed.
+Canonical tfps_linear := AddLinear tfps_is_linear.
 
-Fact val_exp_tfps f (m : nat) :
-  val (f ^+ m) = (val f ^+ m) %% 'X^n.+1.
-Proof.
-elim: m => [|m ihm] //=; first by rewrite expr0 modCXn.
-by rewrite exprS /= ihm modp_mul -exprS.
-Qed.
 
-Lemma hmul_tfpsr1 f : f *h 1 = Tfpsp n (f`_0)%:P.
+(* lalgType structure *)
+Fact scale_tfpsAl c f g : scale_tfps c (f * g) = (scale_tfps c f) * g.
 Proof.
-apply/val_inj/polyP => s; rewrite coef_tfps coef_Tfpsp !coefC.
-by case: s => [|s]; rewrite ?mulr1 ?mulr0.
+by apply tfps_inj; rewrite /= -linearZ  /= !mul_tfps_val -scalerAl linearZ.
 Qed.
+Canonical tfps_lalgType :=
+  Eval hnf in LalgType R {tfps R n} scale_tfpsAl.
+Canonical trXn_lrmorphism := AddLRMorphism trXn_is_linear.
+
 
-Lemma hmul_tfps1r f : 1 *h f = Tfpsp n (f`_0)%:P.
-Proof. by rewrite hmul_tfpsC hmul_tfpsr1. Qed.
+Lemma alg_tfpsC (c : R) : c%:A = c%:S.
+Proof. by apply/tfps_inj; rewrite {1}val_tfpsC -alg_polyC. Qed.
 
-Canonical tfps_comUnitRingType := [comUnitRingType of tfps].
+(* Test *)
+Example trXn_poly0 : trXn n (0 : {poly R}) = 0.
+Proof. by rewrite linear0. Qed.
 
-Lemma unit_tfpsE f : (f \in GRing.unit) = (f`_0 != 0).
-Proof. by rewrite qualifE /= /unit_tfps unitfE. Qed.
+Example trXn_poly1 : trXn n (1 : {poly R}) = 1.
+Proof. by rewrite rmorph1. Qed.
 
-Fact nth0_mul_tfps f g : (f * g)`_0 = f`_0 * g`_0.
-Proof. by rewrite coef_Tfpsp coef0M. Qed.
+Lemma trXnZ (c : R) (p : {poly R}) : trXn n (c *: p) =  c *: (trXn n p).
+Proof. by rewrite linearZ. Qed.
 
-Fact nth0_inv f : (f ^-1)`_0 = (f`_0)^-1.
-Proof.
-have [f_unit|] := boolP (f \is a GRing.unit); first by rewrite coef_inv_tfps.
-move=> fNunit; have := fNunit; rewrite -unitrV; move: fNunit.
-by rewrite !unit_tfpsE !negbK => /eqP -> /eqP ->; rewrite invr0.
-Qed.
 
-Definition scale_tfps (c : K) f := Tfpsp n (c *: (val f)).
+Local Notation "f *h g" := (hmul_tfps f g) (at level 2).
 
-Fact scale_tfpsA a b f : scale_tfps a (scale_tfps b f) = scale_tfps (a * b) f.
-Proof. 
-by apply/val_inj => /=; rewrite modp_scalel modp_mod -modp_scalel scalerA.
+Lemma hmul_tfpsr1 f : f *h 1 = (f`_0)%:S.
+Proof.
+apply/tfpsP => i.
+rewrite coef_tfpsC coef_poly ltnS coef1 => ->.
+by case: i => [|i]; rewrite ?mulr1 ?mulr0.
 Qed.
 
-Fact scale_1tfps : left_id (1 : K) scale_tfps.
+Lemma hmul_tfps1r f : 1 *h f = (f`_0)%:S.
 Proof.
-move=> x; apply/val_inj => /=.
-by rewrite scale1r modp_small // size_polyXn ltnS ?size_tfps.
+apply/tfpsP => i.
+rewrite coef_tfpsC coef_poly ltnS coef1 => ->.
+by case: i => [|i]; rewrite ?mul1r ?mul0r.
 Qed.
 
-Fact scale_tfpsDl f: {morph scale_tfps^~ f : a b / a + b}.
+Lemma tfps_is_cst (g : {tfps R 0}) : g = (g`_0) %:S.
 Proof.
-move=> a b ; apply/val_inj => /=.
-by rewrite scalerDl modp_add.
+apply/tfps_inj; rewrite val_tfpsC.
+by apply: size1_polyC; rewrite size_tfps.
 Qed.
 
-Fact scale_tfpsDr (a : K) : {morph scale_tfps a : f g / f + g}.
-Proof. by move=> f g; apply/val_inj => /=; rewrite scalerDr modp_add. Qed.
 
-Fact scale_tfpsAl (a : K) f g : scale_tfps a (f * g) = scale_tfps a f * g.
-Proof.
-apply/val_inj => /=.
-rewrite modp_scalel modp_small; last by rewrite ltn_modp expf_neq0 // polyX_eq0.
-by rewrite [in RHS]mulrC modp_mul [in RHS]mulrC -modp_scalel -scalerAl.
-Qed.
+Lemma coeftfpsE f i : coeftfps i f = coefp i (tfps f).
+Proof. by rewrite /= coef_tfpsE. Qed.
 
-Definition tfps_lmodMixin := LmodMixin scale_tfpsA scale_1tfps 
-                                                       scale_tfpsDr scale_tfpsDl.
+Fact coeftfps_is_additive i :
+  additive (coeftfps i : {tfps R n} -> R).
+Proof. by move=> f g; exact: coefB. Qed.
+Canonical coeftfps_additive i := Additive (coeftfps_is_additive i).
+Lemma coeftD f g i : (f + g)`_i = f`_i + g`_i.
+Proof. exact: (raddfD (coeftfps_additive i)). Qed.
+Lemma coeftN f i : (- f)`_i = - f`_i.
+Proof. exact: (raddfN (coeftfps_additive i)). Qed.
+Lemma coeftB f g i : (f - g)`_i = f`_i - g`_i.
+Proof. exact: (raddfB (coeftfps_additive i)). Qed.
+Lemma coeftMn f k i : (f *+ k)`_i = f`_i *+ k.
+Proof. exact: (raddfMn (coeftfps_additive i)). Qed.
+Lemma coeftMNn f k i : (f *- k)`_i = f`_i *- k.
+Proof. exact: (raddfMNn (coeftfps_additive i)). Qed.
+Lemma coeft_sum I (r : seq I) (P : pred I) (F : I -> {tfps R n}) k :
+  (\sum_(i <- r | P i) F i)`_k = \sum_(i <- r | P i) (F i)`_k.
+Proof. exact: (raddf_sum (coeftfps_additive k)). Qed.
 
-Canonical tfps_lmodType := Eval hnf in LmodType K tfps tfps_lmodMixin.
-Canonical tfps_lalgType := Eval hnf in LalgType K tfps scale_tfpsAl.
-Canonical tfps_algType := CommAlgType K tfps.
-Canonical unit_tfpsAlgType := Eval hnf in [unitAlgType K of tfps].
+Fact coeftfps_is_linear i :
+  scalable_for *%R (coeftfps i : {tfps R n} -> R).
+Proof. by move=> c g; rewrite /= !coef_tfpsE !linearZ coefZ. Qed.
+Canonical coeftfps_linear i := AddLinear (coeftfps_is_linear i).
 
-Local Notation "c %:S" := (Tfpsp _ (c %:P)) (at level 2).
+Lemma coeftZ a f i : (a *: f)`_i = a * f`_i.
+Proof. exact: (scalarZ [linear of (coeftfps i)]). Qed.
 
-Fact onefE : 1 = 1 %:S.
-Proof. by apply/val_inj => /=; rewrite modCXn. Qed.
 
-End TruncatedPowerSeriesTheory.
+Fact coeftfps0_is_multiplicative :
+  multiplicative (coeftfps 0 : {tfps R n} -> R).
+Proof.
+split=> [p q|]; rewrite !coeftfpsE; last by rewrite polyCK.
+rewrite mul_tfps_val /= -!/(_`_0) coef_trXn /= -!/(_`_0) -!/(coefp 0 _).
+by rewrite rmorphM.
+Qed.
+Canonical coeftfps0_rmorphism := AddRMorphism coeftfps0_is_multiplicative.
+Canonical coeftfps0_lrmorphism := [lrmorphism of coeftfps 0].
 
-Module Notations.
+Fact coef0_tfpsM f g : (f * g)`_0 = f`_0 * g`_0.
+Proof. exact: (rmorphM coeftfps0_rmorphism). Qed.
+Fact coef0_tfpsX f i : (f ^+ i)`_0 = f`_0 ^+ i.
+Proof. exact: (rmorphX coeftfps0_rmorphism). Qed.
 
-Local Open Scope tfps_scope.
+End TFPSTheory.
 
-Notation "{ 'tfps' K n }" := (tfps_of n (Phant K)) : tfps_scope.
-Notation "[ 'tfps' s <= n => F ]" := (tfps_of_fun n (fun s => F)) : tfps_scope.
-Notation "[ 'tfps' s => F ]" := [tfps s <= _ => F] : tfps_scope.
-Notation "c %:S" := (Tfpsp _ (c %:P)) (at level 2) : tfps_scope.
-Notation "f *h g" := (hmul_tfps f g) (at level 2) : tfps_scope.
-Notation "f ^` () " := (deriv_tfps f) (at level 8) : tfps_scope.
 
-End Notations. 
-Import Notations.
+Section TrXnT.
 
-Local Open Scope tfps_scope.
+Variable R : ringType.
+
+Definition trXnt m n : {tfps R m} -> {tfps R n} :=
+  @trXn R n \o (@tfps R m).
 
-Section MoreTruncatedPowerSeries.
+Variables (m n p : nat).
+Implicit Type (f : {tfps R m}).
 
-Lemma Tfpsp_Tfpsp (K : fieldType) (m n : nat) (p : {poly K}) : m <= n ->
-    Tfpsp m (Tfpsp n p) = Tfpsp m p. 
-Proof. by move=> le_mn; apply/val_inj=> /=; rewrite modp_modp // dvdp_exp2l. Qed.
+Lemma coef_trXnt f i : (trXnt n f)`_i = if i <= n then f`_i else 0.
+Proof. by rewrite coef_trXn -coef_tfpsE. Qed.
+
+Lemma trXntE f : trXnt n f = trXn n (tfps f).
+Proof. by []. Qed.
 
-End MoreTruncatedPowerSeries.
+Lemma trXnt_id f : trXnt m f = f.
+Proof. by rewrite /trXnt /= tfpsK. Qed.
 
-Section Truncated_Powerseries.
+Fact trXnt_trXnt f :
+  p <= n -> trXnt p (trXnt n f) = trXnt p f.
+Proof. exact: trXn_trXn. Qed.
 
-Variables (K : fieldType) (n : nat).
+Lemma trXntC a : trXnt n (a%:S : {tfps R m}) = a%:S.
+Proof. exact: trXnCE. Qed.
 
-Fact Tfpsp_is_additive : additive (@Tfpsp K n).
-Proof. by move => f g; apply/val_inj => /=; rewrite modp_add modNp. Qed.
+Lemma trXnt0 : @trXnt m n 0 = 0.
+Proof. exact: trXn0. Qed.
+Lemma trXnt1 : @trXnt m n 1 = 1.
+Proof. exact: trXn1. Qed.
 
-Canonical Tfpsp_additive := Additive Tfpsp_is_additive.
+Fact trXnt_is_linear : linear (@trXnt m n).
+Proof. by move=> c f g; rewrite !trXntE !linearP. Qed.
+Canonical trXnt_additive := Additive trXnt_is_linear.
+Canonical trXnt_linear := AddLinear trXnt_is_linear.
 
-Lemma Tfpsp_is_multiplicative: multiplicative (@Tfpsp K n).
+Hypothesis H : n <= m.
+Fact trXnt_is_multiplicative : multiplicative (@trXnt m n).
 Proof.
-split => [f g|]; last by apply/val_inj => /=; rewrite modCXn.
-by apply/val_inj => /=; rewrite modp_mul [in RHS]mulrC modp_mul mulrC.
+split=> [f g|] /=; last exact trXnt1.
+rewrite /trXnt /= mul_tfps_val /=.
+by rewrite -rmorphM /= trXn_trXn.
 Qed.
+Canonical trXnt_multiplicative := AddRMorphism trXnt_is_multiplicative.
+Canonical trXnt_lrmorphism := AddLRMorphism trXnt_is_linear.
 
-Canonical Tfpsp_rmorphism := AddRMorphism Tfpsp_is_multiplicative.
+End TrXnT.
 
-Fact TfpspZ (c : K) (p : {poly K}): (Tfpsp n (c *: p))=  c *:(Tfpsp n p).
-Proof. by apply/val_inj => /=; rewrite -modp_scalel modp_mod. Qed.
 
-Canonical Tfpsp_linear := AddLinear TfpspZ.
+Section TestTrXnT.
 
-Canonical Tfpsp_lrmorphism := [lrmorphism of (Tfpsp n)].
+Variable R : ringType.
+Variables (m n p : nat).
+Implicit Type (f g : {tfps R m}).
 
-(* tests *)
-Fact tfps0 : Tfpsp n (0 : {poly K}) = 0.
+(* Test *)
+Example trXnt_tfps0 : trXnt n (0 : {tfps R m}) = 0.
 Proof. by rewrite linear0. Qed.
 
-Fact tfps1 : Tfpsp n (1 : {poly K}) = 1.
+Example trXn_tfps1 : trXn n (tfps (1 : {tfps R m})) = 1.
 Proof. by rewrite rmorph1. Qed.
 
-Lemma Tfpsp_is_unit (p : {poly K}) :
-                                    ((Tfpsp n p) \is a GRing.unit) = (p`_0 != 0).
-Proof. by rewrite unit_tfpsE nth0_Tfpsp. Qed.
+Example trXntZ c f : trXnt n (c *: f) =  c *: (trXnt n f).
+Proof. by rewrite linearZ. Qed.
 
-Lemma TfpspE (p : {poly K}) : p %% 'X^ n.+1 = Tfpsp n p.
-Proof. by apply/val_inj => /=. Qed.
+Example trXntM f g : n <= m -> trXnt n (f * g) = trXnt n f * trXnt n g.
+Proof. by move=> H; rewrite rmorphM. Qed.
 
-End Truncated_Powerseries.
+Example trXntM12 (f g : {tfps R 2}) :
+  trXnt 1 (f * g) =  (trXnt 1 f) * (trXnt 1 g).
+Proof. by rewrite rmorphM. Qed.
 
-Section MapTfps.
+End TestTrXnT.
 
-Variables (K L : fieldType) (n : nat) (f : {rmorphism K -> L}).
 
-Implicit Type g h : {tfps K n}.
+Section TFPSX.
 
-Definition map_tfps g := Tfpsp n (map_poly f (val g)).
+Variable (R : ringType) (n : nat).
+Implicit Types (f g : {tfps R n}).
 
-Lemma map_tfpsM g h : map_tfps (g * h) = (map_tfps g) * (map_tfps h).
+Lemma tfps0X m : m = 0%N -> \Xo(m) = 0 :> {tfps R m}.
 Proof.
-apply/val_inj => /=.
-rewrite map_modp rmorphX /= map_polyX modp_mod rmorphM modp_mul.
-by rewrite [in RHS]mulrC modp_mul mulrC.
+by move=> ->; rewrite (tfps_is_cst \X) coef_trXn coefX /= tfpsC0.
 Qed.
 
-Fact map_tfps_is_additive : additive map_tfps.
+Lemma val_tfpsSX m : tfps (\Xo(m.+1)) = 'X%R :> {poly R}.
 Proof.
-move => x y; apply/val_inj => /=.
-by rewrite rmorphB /= modp_add modNp.
+apply/polyP => i.
+by rewrite coef_trXn coefX; case: eqP => [->|] // _; rewrite if_same.
 Qed.
 
-Canonical map_tfps_additive := Additive map_tfps_is_additive.
+Lemma val_tfpsX m : tfps (\Xo(m)) = (m != 0%N)%:R *: 'X%R :> {poly R}.
+Proof.
+case: m => [|m]; first by rewrite tfps0X /= ?scale0r.
+by rewrite val_tfpsSX /= scale1r.
+Qed.
 
-Fact map_tfps_is_multiplicative : multiplicative map_tfps.
-Proof. 
-split => [x y|]; first by rewrite map_tfpsM.
-by apply/val_inj => /=; rewrite rmorph1 modCXn.
+Lemma coef_tfpsX m i :
+  (\X : {tfps R m})`_i = (m != 0%N)%:R * (i == 1%N)%:R.
+Proof. by rewrite coef_tfpsE val_tfpsX coefZ coefX. Qed.
+
+Lemma trXn_tfpsX m : @trXn R n (tfps \Xo(m.+1)) = \X.
+Proof.
+case: n => [|n'].
+  rewrite [RHS]tfps0X //; apply tfpsP => i.
+  rewrite leqn0 => /eqP ->.
+  by rewrite coef_tfps0 coef_trXn -coef_tfpsE coef_tfpsX /= mulr0.
+by apply tfps_inj; rewrite !val_tfpsSX.
 Qed.
 
-Canonical map_tfps_rmorphism := AddRMorphism map_tfps_is_multiplicative.
+Lemma trXnt_tfpsX m : @trXnt R _ n \Xo(m.+1) = \X.
+Proof. exact: trXn_tfpsX. Qed.
+
+Lemma commr_tfpsX f : GRing.comm f \X.
+Proof.
+apply/tfpsP => i _.
+by rewrite !mul_tfps_val /= trXn_mull trXn_mulr commr_polyX.
+Qed.
 
-Lemma map_tfpsZ (c : K) g : (map_tfps (c *: g)) =  (f c) *: (map_tfps g).
+Lemma expr_cX (c : R) i : (c *: \Xo(n)) ^+ i = (c ^+ i) *: \X ^+ i.
 Proof.
-apply/val_inj => /=.
-by rewrite map_modp rmorphX /= map_polyX linearZ [in LHS]modp_scalel.
+rewrite -mulr_algl exprMn_comm; last exact: commr_tfpsX.
+by rewrite -in_algE -rmorphX /= mulr_algl.
 Qed.
 
-Lemma tfps_is_cst (g : tfps K 0%N) : g = (g`_0) %:S.
+Lemma coef_tfpsXM f i :
+  (\X * f)`_i = if i == 0%N then 0 else if i <= n then f`_i.-1 else 0.
+Proof. by rewrite !mul_tfps_val /= trXn_mull coef_trXn coefXM; case: i. Qed.
+
+Lemma coef_tfpsXnM f k i :
+  (\X ^+ k * f)`_i = if i < k then 0 else if i <= n then f`_(i - k) else 0.
 Proof.
-by apply/val_inj=> /=; rewrite modCXn //; apply: size1_polyC; rewrite size_tfps.
+elim: k i => [|k IHk] i.
+  by rewrite expr0 ltn0 mul1r subn0 {1}coef_tfps.
+rewrite exprS -mulrA coef_tfpsXM {}IHk.
+case: i => [|i]//=; rewrite ltnS subSS.
+by case: (ltnP i n) => [/ltnW ->|]//; rewrite if_same.
 Qed.
 
-(* used once; to remove ? *)
-Lemma tfpsC_mul : {morph (fun x => (x%:S : {tfps K n})) : a b / a * b >-> a * b}.
+Lemma coef_tfpsXn i k :
+  ((\X : {tfps R n})^+ k)`_i = ((i <= n) && (i == k%N))%:R.
 Proof.
-move=> a b; apply/val_inj => /=; rewrite polyC_mul modp_mul.
-by rewrite [in RHS]mulrC modp_mul mulrC.
+rewrite -[_ ^+ k]mulr1 coef_tfpsXnM coef1 -/(leq _ _).
+case: (altP (i =P k)) => [-> | Hneq]; first by rewrite ltnn leqnn; case: leqP.
+case: (leqP i n) => _; last by rewrite if_same.
+case: ltnP => //=.
+by rewrite [i <= k]leq_eqVlt (negbTE Hneq) ltnNge => ->.
 Qed.
 
-Canonical map_tfps_linear := let R := ({tfps K n}) in
-                       AddLinear (map_tfpsZ : scalable_for (f \; *:%R) map_tfps).
+Lemma tfps_def f : f = \sum_(i < n.+1) f`_i *: \X ^+ i.
+Proof.
+apply/tfpsP => j le_jn; have:= le_jn; rewrite -ltnS => lt_jn1.
+rewrite coeft_sum /= (bigD1 (Ordinal lt_jn1)) //=.
+rewrite coeftZ coef_tfpsXn eqxx le_jn mulr1.
+rewrite big1 ?addr0 // => [[i /= Hi]]; rewrite -val_eqE /= => Hneq.
+by rewrite coeftZ coef_tfpsXn eq_sym (negbTE Hneq) andbF mulr0.
+Qed.
 
-Canonical map_tfps_lrmorphism := [lrmorphism of map_tfps].
+End TFPSX.
 
-(* tests *)
-Fact test_map_tfps0 : map_tfps 0 = 0.
-Proof. by rewrite linear0. Qed.
 
-Fact test_map_tfpsD g h : map_tfps (g + h) = (map_tfps g) + (map_tfps h).
-Proof. by rewrite linearD. Qed.
+Section TFPSConvRing.
+
+Variable (R : ringType) (n : nat).
 
-Lemma Tfps_map_poly (p : {poly K}) :
-                     @Tfpsp L n (p ^ f) = map_tfps (Tfpsp n p).
-Proof. by apply/val_inj => /=; rewrite map_modp map_polyXn modp_mod. Qed.
+Fact size_convr_subproof (f : {tfps R n}) :
+  size (map_poly (fun c : R => c : R^c) (tfps f)) <= n.+1.
+Proof. by rewrite size_map_inj_poly ?size_tfps. Qed.
+Definition convr_tfps f : {tfps R^c n} := Tfps_of (size_convr_subproof f).
 
-Local Notation "g ^ f" := (map_tfps g) : tfps_scope.
+Fact size_iconvr_subproof (f : {tfps R^c n}) :
+  size (map_poly (fun c : R^c => c : R) (tfps f)) <= n.+1.
+Proof. by rewrite size_map_inj_poly ?size_tfps. Qed.
+Definition iconvr_tfps f : {tfps R n} := Tfps_of (size_iconvr_subproof f).
 
-Lemma map_hmul g h : (g *h h) ^ f = (g ^ f) *h (h ^ f).
+Fact convr_tfps_is_additive : additive convr_tfps.
 Proof.
-apply/val_inj => /=; rewrite -polyP => i.
-rewrite coef_modXn coef_map 2!coef_poly !coef_modXn.
-by case: (i < n.+1) => //=; rewrite rmorphM !coef_map.
+by move=> f g; apply/tfpsP => i _; rewrite /= coefB !coef_map_id0 // coefB.
 Qed.
+Canonical convr_tfps_additive := Additive convr_tfps_is_additive.
 
-Lemma map_tfps_injective : injective map_tfps.
+Fact iconvr_tfps_is_additive : additive iconvr_tfps.
 Proof.
-move => x y; move/val_eqP => /=.
-rewrite ?(modp_small, (size_polyXn, size_map_poly, ltnS, size_tfps)) //.
-by move/val_eqP => H; move: (map_poly_inj f H); apply/val_inj.
+by move=> f g; apply/tfpsP => i _; rewrite /= coefB !coef_map_id0 // coefB.
 Qed.
+Canonical iconvr_tfps_additive := Additive iconvr_tfps_is_additive.
 
-End MapTfps.
+Lemma convr_tfpsK : cancel convr_tfps iconvr_tfps.
+Proof. by move=> f; apply/tfpsP => i _; rewrite !coef_map_id0. Qed.
+Lemma iconvr_tfpsK : cancel iconvr_tfps convr_tfps.
+Proof. by move=> f; apply/tfpsP => i _; rewrite !coef_map_id0. Qed.
 
-Section IdFun.
+Lemma convr_tfps1 : convr_tfps 1 = 1.
+Proof. by apply/tfpsP => i Hi; rewrite coef_map_id0 // !coef1. Qed.
+Lemma iconvr_tfps1 : iconvr_tfps 1 = 1.
+Proof. by apply/tfpsP => i Hi; rewrite coef_map_id0 // !coef1. Qed.
 
-Lemma map_poly_idfun (R : ringType) : map_poly (@idfun R) =1 @idfun {poly R}.
-Proof. exact: coefK. Qed.
-
-Lemma idfun_injective A : injective (@idfun A). Proof. done. Qed.
-Canonical idfun_is_injmorphism (A : ringType) := 
-    InjMorphism (@idfun_injective A).
-
-End IdFun.
-
-Lemma map_powerseries_idfun (K : fieldType) (m : nat) : 
-  map_tfps [rmorphism of (@idfun K)] =1 @idfun ({tfps K m}).
-Proof. 
-move => p; apply: val_inj => /=.
-by rewrite map_poly_idfun modp_small // size_polyXn ltnS size_tfps.
+Lemma convr_tfpsM f g :
+  convr_tfps f * convr_tfps g = convr_tfps (g * f).
+Proof.
+apply/tfpsP => i Hi.
+rewrite coefM_tfps coef_map_id0 // coefMr_tfps Hi.
+by apply eq_bigr => j _ /=; rewrite !coef_map_id0.
+Qed.
+Lemma iconvr_tfpsM f g :
+  iconvr_tfps f * iconvr_tfps g = iconvr_tfps (g * f).
+Proof.
+apply/tfpsP => i Hi.
+rewrite coefM_tfps coef_map_id0 // coefMr_tfps Hi.
+by apply eq_bigr => j _ /=; rewrite !coef_map_id0.
 Qed.
 
-Section Coefficient01.
+End TFPSConvRing.
 
-Variables (K : fieldType) (n : nat).
 
-Implicit Types (f g : {tfps K n}).
+Section TFPSComRing.
 
-Definition coef0_is_0 : pred_class := fun f : {tfps K n} => f`_0 == 0.
+Variable (R : comRingType) (n : nat).
+Implicit Types (f g : {tfps R n}).
 
-Lemma coef0_is_0E f : (f \in coef0_is_0) = (f`_0 == 0).
-Proof. by rewrite -topredE. Qed.
+Fact mul_tfpsC f g : f * g = g * f.
+Proof. by rewrite !mul_tfps_val mulrC. Qed.
+Canonical tfps_comRingType :=
+  Eval hnf in ComRingType {tfps R n} mul_tfpsC.
+Canonical tfps_algType := Eval hnf in CommAlgType R {tfps R n}.
 
-Definition coef0_is_1 : pred_class := fun f : {tfps K n} => f`_0 == 1.
+Lemma hmul_tfpsC : commutative (@hmul_tfps R n).
+Proof. by move=> f1 f2; apply/tfpsP => i; rewrite !coef_poly mulrC. Qed.
 
-Lemma coef0_is_1E f : (f \in coef0_is_1) = (f`_0 == 1).
-Proof. by rewrite -topredE. Qed.
+End TFPSComRing.
 
-Definition exp f :=
-  if f \notin coef0_is_0 then 0 else
-  Tfpsp n (\sum_(i < n.+1) ((i`! %:R) ^-1) *: (val f ^+i)).
 
-Definition log f :=
-  if f \notin coef0_is_1 then 0 else
-  Tfpsp n (- \sum_(1 <= i < n.+1) ((i %:R) ^-1) *: ((1 - val f) ^+i)).
+Section TFPSUnitRingLeft.
 
-Fact c0_is_0_idealr : idealr_closed coef0_is_0.
-Proof. 
-split => [|| a p q ]; rewrite ?coef0_is_0E ?coefC ?eqxx ?oner_eq0 //.
-move=> /eqP p0_eq0 /eqP q0_eq0.
-by rewrite coefD q0_eq0 addr0 nth0_mul_tfps p0_eq0 mulr0.
-Qed.
+Variable (R : unitRingType) (n : nat).
+Implicit Types (f g : {tfps R n}).
 
-Fact c0_is_0_key : pred_key coef0_is_0. Proof. by []. Qed.
+Definition unit_tfps : pred {tfps R n} := fun f => f`_0 \in GRing.unit.
 
-Canonical c0_is_0_keyed := KeyedPred c0_is_0_key.
-Canonical c0_is_0_opprPred := OpprPred c0_is_0_idealr. 
-Canonical c0_is_0_addrPred := AddrPred c0_is_0_idealr. 
-Canonical c0_is_0_zmodPred := ZmodPred c0_is_0_idealr.
+Fixpoint inv_tfps_rec f bound m :=
+  if bound is b.+1 then
+    if (m <= b)%N then inv_tfps_rec f b m
+    else -f`_0%N^-1 * (\sum_(i < m) f`_i.+1 * (inv_tfps_rec f b (m - i.+1)%N))
+  else f`_0%N^-1.
+Definition inv_tfps f : {tfps R n} :=
+  if unit_tfps f then [tfps i <= n => inv_tfps_rec f i i] else f.
 
-Definition c0_is_0_ntideal := idealr_closed_nontrivial c0_is_0_idealr.
+Lemma coef0_inv_tfps f : unit_tfps f -> (inv_tfps f)`_0 = f`_0^-1.
+Proof. by rewrite /inv_tfps => ->; rewrite coef_tfps_of_fun. Qed.
 
-Canonical c0_is_0_ideal := MkIdeal c0_is_0_zmodPred c0_is_0_ntideal.
+Lemma coefS_inv_tfps f m :
+  unit_tfps f -> m < n ->
+  (inv_tfps f)`_m.+1 =
+  - f`_0%N^-1 *
+    (\sum_(i < m.+1) f`_i.+1 * (inv_tfps f)`_(m - i)%N).
+Proof.
+move=> s_unit lt_mn.
+rewrite /inv_tfps s_unit coef_tfps_of_fun /= ltnn lt_mn; congr (- _ * _).
+apply: eq_bigr => [[i]/=]; rewrite ltnS => le_im _.
+rewrite coef_tfps_of_fun (leq_trans (leq_subr _ _) (ltnW lt_mn)).
+congr (_ * _); rewrite /bump /= subSS.
+move: (m - i)%N (leq_subr i m) {le_im} => {}i le_im.
+move: le_im => /subnKC <-; elim: (m - i)%N => [|k IHl]; first by rewrite addn0.
+by rewrite addnS /= leq_addr.
+Qed.
 
-Fact c0_is_0_prime : prime_idealr_closed coef0_is_0.
-Proof. 
-by move => x y; rewrite -!topredE /= /coef0_is_0 nth0_mul_tfps mulf_eq0. 
+Lemma mul_tfpsVr : {in unit_tfps, right_inverse 1 inv_tfps *%R}.
+Proof.
+move=> f s_unit; have:= s_unit; rewrite /= unfold_in => s0_unit.
+apply/tfpsP => m _; elim: m {1 3 4}m (leqnn m) => [| m IHm] i.
+  rewrite leqn0 => /eqP ->.
+  by rewrite coef1 coef0_tfpsM coef0_inv_tfps ?divrr.
+move=> le_im1; case: (leqP i m) => [|lt_mi]; first exact: IHm.
+have {le_im1 lt_mi i} -> : i = m.+1 by apply anti_leq; rewrite le_im1 lt_mi.
+rewrite coef1 [RHS]/=.
+case: (ltnP m.+1 n.+1) => Hmn; last first.
+  by rewrite nth_default ?(leq_trans (size_tfps _)).
+rewrite coefM_tfps -ltnS Hmn big_ord_recl [val ord0]/= subn0.
+rewrite coefS_inv_tfps // mulNr mulrN mulVKr // addrC.
+apply/eqP; rewrite subr_eq0; apply/eqP.
+by apply eq_bigr => [] [i] /=.
 Qed.
 
-Canonical coef0_is_0_pideal := MkPrimeIdeal c0_is_0_ideal c0_is_0_prime.
+Lemma inv_tfps0id : {in [predC unit_tfps], inv_tfps =1 id}.
+Proof.
+by move=> s; rewrite inE /= /inv_tfps unfold_in /unit_tfps => /negbTE ->.
+Qed.
 
-(* tests *)
-Example zero_in_coef0_is_0 : 0 \in coef0_is_0.
-Proof. by rewrite rpred0. Qed.
+End TFPSUnitRingLeft.
 
-Example coef0_is_0D f g : 
-    f \in coef0_is_0 -> g \in coef0_is_0 -> f + g \in coef0_is_0.
-Proof. by move=> hf hg; rewrite rpredD. Qed.
 
-Example coef0_os_0N f : f \in coef0_is_0 -> (-f) \in coef0_is_0.
-Proof. by move=> hf; rewrite rpredN. Qed.
+Section TruncFPSUnitRing.
 
-Example coef0_is_0_prime_test f g : 
-    f * g \in coef0_is_0 -> (f \in coef0_is_0) || (g \in coef0_is_0).
+Variable (R : unitRingType) (n : nat).
+Implicit Types (f g : {tfps R n}).
+
+Let invl_tfps f := iconvr_tfps (inv_tfps (convr_tfps f)).
+
+Fact mul_tfpsVl : {in @unit_tfps R n, left_inverse 1 invl_tfps *%R}.
+Proof.
+move=> f Hf; rewrite /invl_tfps -{2}(convr_tfpsK f).
+rewrite iconvr_tfpsM mul_tfpsVr ?iconvr_tfps1 //.
+by move: Hf; rewrite !unfold_in coef_map_id0.
+Qed.
+
+(* General semi-group theory : left inverse = right inverse *)
+Fact invr_tfpsE f : unit_tfps f -> inv_tfps f = invl_tfps f.
+Proof.
+move=> H; have:= erefl (invl_tfps f * f * inv_tfps f).
+by rewrite -{2}mulrA mul_tfpsVl // mul1r mul_tfpsVr // mulr1.
+Qed.
+
+Lemma mul_tfpsrV :
+  {in @unit_tfps R n, left_inverse 1 (@inv_tfps R n) *%R}.
+Proof. by move=> f Hs; rewrite invr_tfpsE // mul_tfpsVl. Qed.
+
+Lemma unit_tfpsP f g : g * f = 1 /\ f * g = 1 -> unit_tfps f.
+Proof.
+move=> [] /(congr1 (fun x : {tfps _ _ } => x`_0)).
+rewrite coef1 coef0_tfpsM => Hl.
+move=>    /(congr1 (fun x : {tfps _ _ } => x`_0)).
+rewrite coef1 coef0_tfpsM => Hr.
+by rewrite /unit_tfps; apply/unitrP; exists g`_0.
+Qed.
+
+Definition tfps_unitMixin :=
+  UnitRingMixin mul_tfpsrV (@mul_tfpsVr R n) unit_tfpsP (@inv_tfps0id R n).
+Canonical tfps_unitRingType :=
+  Eval hnf in UnitRingType {tfps R n} tfps_unitMixin.
+
+
+Lemma unit_tfpsE f : (f \in GRing.unit) = (f`_0 \in GRing.unit).
+Proof. by []. Qed.
+
+Lemma trXn_unitE (p : {poly R}) :
+  ((trXn n p) \is a GRing.unit) = (p`_0 \is a GRing.unit).
+Proof. by rewrite unit_tfpsE coef0_trXn. Qed.
+
+Lemma coef0_tfpsV f : (f ^-1)`_0 = (f`_0)^-1.
+Proof.
+case (boolP (f \is a GRing.unit))=> [f_unit|]; first by rewrite coef0_inv_tfps.
+move=> Hinv; rewrite (invr_out Hinv).
+by move: Hinv; rewrite unit_tfpsE => /invr_out ->.
+Qed.
+
+Lemma coef_tfpsV f i : f \is a GRing.unit -> f^-1`_i =
+  if i > n then 0 else
+  if i == 0%N then f`_0 ^-1
+  else - (f`_0 ^-1) * (\sum_(j < i) f`_j.+1 * f^-1`_(i - j.+1)).
+Proof.
+move=> funit; case: ltnP => Hi.
+  by rewrite -(tfpsK f^-1) coef_trXnt (ltn_geF Hi).
+case: i Hi => [|i] Hi; first by rewrite eq_refl coef0_tfpsV.
+by rewrite coefS_inv_tfps.
+Qed.
+
+Lemma tfpsCV (c : R) : (trXn n c%:P)^-1 = trXn n (c^-1)%:P.
+Proof.
+case (boolP (c \in GRing.unit)) => [Uc | nUc].
+  by rewrite -/((trXn n \o @polyC R) _) -rmorphV.
+by rewrite !invr_out // unit_tfpsE coef_trXn coefC.
+Qed.
+
+End TruncFPSUnitRing.
+
+
+Section TruncFPSTheoryUnitRing.
+
+Variable (R : unitRingType) (m n : nat).
+Implicit Types (f g : {tfps R n}).
+
+Lemma trXnt_unitE f :
+  ((trXnt m f) \is a GRing.unit) = (f`_0 \is a GRing.unit).
+Proof. exact: trXn_unitE. Qed.
+
+Lemma trXntV f : m <= n -> trXnt m (f^-1) = (trXnt m f) ^-1.
+Proof.
+move=> leq_mn.
+case (boolP (f`_0 \is a GRing.unit)) => f0U; first last.
+  by rewrite !invr_out // unit_tfpsE ?coef0_trXn.
+by rewrite rmorphV.
+Qed.
+
+End TruncFPSTheoryUnitRing.
+
+
+Section TFPSComUnitRing.
+
+Variable (R : comUnitRingType) (n : nat).
+Implicit Types (f g : {tfps R n}).
+
+Canonical tfps_comUnitRingType := [comUnitRingType of {tfps R n}].
+Canonical tfps_unitAlgType := Eval hnf in [unitAlgType R of {tfps R n}].
+
+End TFPSComUnitRing.
+
+
+Section TFPSIDomain.
+
+Variable R : idomainType.
+
+Lemma poly_modXn n (p : {poly R}) : p %% 'X^n = Poly (take n p).
+Proof.
+rewrite -{1}(poly_cat p n) addrC mulrC Pdiv.IdomainUnit.modp_addl_mul_small //.
+- by rewrite lead_coefXn unitr1.
+- rewrite size_polyXn ltnS (leq_trans (size_Poly _)) //.
+  by rewrite size_take -/(minn _ _) geq_minl.
+Qed.
+
+Lemma trXn_modE m (p : {poly R}) : p %% 'X^ m.+1 = tfps (trXn m p).
+Proof. by apply/val_inj => /=; rewrite trXnE poly_modXn. Qed.
+
+Fact tfps_modp (n m : nat) (p : {poly R}) : n <= m ->
+  trXn n (p %% 'X^m.+1) = trXn n p.
+Proof. by move=> lt_nm; apply/val_inj; rewrite /= trXn_modE trXn_trXn. Qed.
+
+Variable n : nat.
+Implicit Types (f g : {tfps R n}).
+
+Fact mod_tfps (m : nat) f : n <= m -> (tfps f) %% 'X^m.+1 = (tfps f).
+Proof.
+move=> leq_nm.
+by rewrite modp_small // size_polyXn ltnS (leq_trans (size_tfps _)).
+Qed.
+
+End TFPSIDomain.
+
+
+Section MapTFPS.
+
+Variables (K L : ringType) (n : nat) (f : {rmorphism K -> L}).
+
+Implicit Type g h : {tfps K n}.
+
+Fact map_tfps_subproof g : size (map_poly f (val g)) <= n.+1.
+Proof.
+by rewrite map_polyE (leq_trans (size_Poly _)) // size_map size_tfps.
+Qed.
+Definition map_tfps g := Tfps_of (map_tfps_subproof g).
+
+Lemma map_tfpsM g h : map_tfps (g * h) = (map_tfps g) * (map_tfps h).
+Proof.
+apply/tfpsP => i Hi.
+rewrite coef_map /= !coefM_tfps Hi rmorph_sum.
+apply eq_bigr => [] [j]; rewrite /= ltnS => le_ji _.
+by rewrite rmorphM !coef_map.
+Qed.
+
+Fact map_tfps_is_additive : additive map_tfps.
+Proof. by move => x y; apply/tfps_inj => /=; rewrite rmorphB. Qed.
+Canonical map_tfps_additive := Additive map_tfps_is_additive.
+
+Lemma map_tfpsZ (c : K) g : map_tfps (c *: g) = (f c) *: (map_tfps g).
+Proof. by apply/tfpsP => i le_in; rewrite coef_tfpsE /= map_polyZ. Qed.
+Canonical map_tfps_linear := let R := {tfps K n} in
+  AddLinear (map_tfpsZ : scalable_for (f \; *:%R) map_tfps).
+
+Fact map_tfps_is_multiplicative : multiplicative map_tfps.
+Proof.
+split => [x y|]; first by rewrite map_tfpsM.
+by apply/tfps_inj => /=; rewrite rmorph1.
+Qed.
+Canonical map_tfps_rmorphism := AddRMorphism map_tfps_is_multiplicative.
+Canonical map_tfps_lrmorphism := [lrmorphism of map_tfps].
+
+
+(* Tests *)
+Example test_map_tfps0 : map_tfps 0 = 0.
+Proof. by rewrite linear0. Qed.
+
+Example test_map_tfpsD g h :
+  map_tfps (g + h) = (map_tfps g) + (map_tfps h).
+Proof. by rewrite linearD. Qed.
+
+
+Lemma trXn_map_poly (p : {poly K}) :
+  @trXn L n (map_poly f p) = map_tfps (trXn n p).
+Proof. by apply/tfpsP => i le_in; rewrite !(coef_trXn, le_in, coef_map). Qed.
+
+Local Notation "g '^f'" := (map_tfps g).
+Local Notation "f *h g" := (hmul_tfps f g) (at level 2).
+
+Lemma map_hmul g h : (g *h h) ^f = (g ^f) *h (h ^f).
+Proof.
+apply/tfpsP => i le_in /=.
+rewrite coef_map !coef_poly ltnS le_in [LHS]rmorphM.
+have co (l : {tfps K n}) : (if i < size l then f l`_i else 0) = f l`_i.
+  by case: ltnP => // H; rewrite nth_default // rmorph0.
+by rewrite !co.
+Qed.
+
+End MapTFPS.
+
+Lemma map_tfps_injective (K L : ringType) n (f : {injmorphism K -> L}) :
+  injective (@map_tfps _ _ n f).
+Proof.
+by move=> x y /val_eqP/eqP /= /map_poly_injective H; apply tfps_inj.
+Qed.
+
+Lemma map_tfps_inj (K : fieldType) (L : ringType) n (f : {rmorphism K -> L}) :
+  injective (@map_tfps _ _ n f).
+Proof. by move=> x y /val_eqP/eqP /= /map_poly_inj H; apply tfps_inj. Qed.
+
+Lemma trXnt_map_poly (m n : nat) (K L : ringType)
+      (f : {rmorphism K -> L}) (g : {tfps K n}) :
+  trXnt m (map_tfps f g) = map_tfps f (trXnt m g).
+Proof. by apply/tfpsP=> i le_in; rewrite !(coef_map, coef_trXn) le_in. Qed.
+
+Lemma map_poly_idfun (R : ringType) : map_poly (@idfun R) =1 @idfun {poly R}.
+Proof. exact: coefK. Qed.
+
+Lemma idfun_injective A : injective (@idfun A). Proof. done. Qed.
+Canonical idfun_is_injmorphism (A : ringType) :=
+    InjMorphism (@idfun_injective A).
+
+Lemma map_tfps_idfun (K : fieldType) (m : nat) :
+  map_tfps [rmorphism of (@idfun K)] =1 @idfun {tfps K m}.
+Proof.
+move=> f; apply/tfpsP => i le_in /=.
+by rewrite coef_tfpsE /= map_poly_idfun.
+Qed.
+
+
+Section Coefficient01.
+
+Variables (R : ringType) (n : nat).
+Implicit Types (f g : {tfps R n}).
+
+Definition coef0_eq0 := fun f : {tfps R n} => f`_0 == 0.
+Definition coef0_eq1 := fun f : {tfps R n} => f`_0 == 1.
+
+Lemma coef0_eq0E f : (f \in coef0_eq0) = (f`_0 == 0).
+Proof. by rewrite -topredE. Qed.
+
+Lemma coef0_eq1E f : (f \in coef0_eq1) = (f`_0 == 1).
+Proof. by rewrite -topredE. Qed.
+
+Fact coef0_eq0_idealr : idealr_closed coef0_eq0.
+Proof.
+split => [|| a p q ]; rewrite ?coef0_eq0E ?coefC ?eqxx ?oner_eq0 //.
+move=> /eqP p0_eq0 /eqP q0_eq0.
+by rewrite coefD q0_eq0 addr0 coef0_tfpsM p0_eq0 mulr0.
+Qed.
+
+Fact coef0_eq0_key : pred_key coef0_eq0. Proof. by []. Qed.
+
+Canonical coef0_eq0_keyed := KeyedPred coef0_eq0_key.
+Canonical coef0_eq0_opprPred := OpprPred coef0_eq0_idealr.
+Canonical coef0_eq0_addrPred := AddrPred coef0_eq0_idealr.
+Canonical coef0_eq0_zmodPred := ZmodPred coef0_eq0_idealr.
+
+Definition coef0_eq0_ntideal := idealr_closed_nontrivial coef0_eq0_idealr.
+Canonical coef0_eq0_ideal := MkIdeal coef0_eq0_zmodPred coef0_eq0_ntideal.
+
+Lemma coef0_eq0Z f c : f \in coef0_eq0 -> c *: f \in coef0_eq0.
+Proof. by move=> hf; rewrite -mulr_algl idealMr. Qed.
+
+Lemma coef0_eq0X f i : f \in coef0_eq0 -> f ^+ i.+1 \in coef0_eq0.
+Proof. by move=> hf; rewrite exprSr idealMr. Qed.
+
+Lemma coef0_eq10 f : (f \in coef0_eq1) = ((1 - f) \in coef0_eq0).
+Proof. by rewrite ?coef0_eq0E ?coef0_eq1E coefB coef1 subr_eq0 eq_sym. Qed.
+
+Lemma coef0_eq01 f : (f \in coef0_eq0) = ((1 + f) \in coef0_eq1).
+Proof. by rewrite coef0_eq10 -[RHS]rpredN !opprD !opprK addKr. Qed.
+
+Lemma coef0_eq1_add01 f g :
+  f \in coef0_eq0 -> g \in coef0_eq1 -> f + g \in coef0_eq1.
+Proof.
+rewrite coef0_eq0E !coef0_eq1E coefD => /eqP -> /eqP ->.
+by rewrite add0r.
+Qed.
+
+Lemma tfpsX_in_coef0_eq0 : \X \in coef0_eq0.
+Proof. by rewrite coef0_eq0E coef_trXn coefX. Qed.
+
+(* tests *)
+Example zero_in_coef0_eq0 : 0 \in coef0_eq0.
+Proof. by rewrite rpred0. Qed.
+
+Example coef0_eq0D f g :
+    f \in coef0_eq0 -> g \in coef0_eq0 -> f + g \in coef0_eq0.
+Proof. by move=> hf hg; rewrite rpredD. Qed.
+
+Example coef0_eq0N f : f \in coef0_eq0 -> (-f) \in coef0_eq0.
+Proof. by move=> hf; rewrite rpredN. Qed.
+
+
+Fact mulr_closed_coef0_eq1 : mulr_closed coef0_eq1.
+Proof.
+split=> [|x y]; rewrite !coef0_eq1E ?coefC //.
+by rewrite coef0_tfpsM; move/eqP ->; move/eqP ->; rewrite mul1r.
+Qed.
+Fact coef0_eq1_key : pred_key coef0_eq1. Proof. by []. Qed.
+Canonical coef0_eq1_keyed := KeyedPred coef0_eq1_key.
+Canonical coef0_eq1_MulrPred := MulrPred mulr_closed_coef0_eq1.
+
+(* Tests *)
+Example one_in_coef0_eq1 : 1 \in coef0_eq1.
+Proof. by rewrite rpred1. Qed.
+
+Example coef0_eq1M f g :
+  f \in coef0_eq1 -> g \in coef0_eq1 -> f * g \in coef0_eq1.
+Proof. by move=> hf hg; rewrite rpredM. Qed.
+
+End Coefficient01.
+Arguments coef0_eq0 {R n}.
+Arguments coef0_eq1 {R n}.
+
+Lemma coef0_eq0_trXnt (R : ringType) (n m : nat) (f : {tfps (R) n}) :
+  (trXnt m f \in coef0_eq0) = (f \in coef0_eq0).
+Proof. by rewrite !coef0_eq0E coef0_trXn. Qed.
+
+Lemma coef0_eq1_trXnt (R : ringType) (n m : nat) (f : {tfps (R) n}) :
+  (trXnt m f \in coef0_eq1) = (f \in coef0_eq1).
+Proof. by rewrite !coef0_eq1E coef0_trXn. Qed.
+
+
+Section Coefficient01Unit.
+
+Variables (R : unitRingType) (n : nat).
+Implicit Types (f g : {tfps R n}).
+
+Fact invr_closed_coef0_eq1 : invr_closed (@coef0_eq1 R n).
+Proof.
+move=> f; rewrite !coef0_eq1E coef0_tfpsV; move/eqP ->.
+by rewrite invr1.
+Qed.
+Canonical coef0_eq1_DivrPred := DivrPred invr_closed_coef0_eq1.
+
+Lemma coef0_eq1V f : f \in coef0_eq1 -> f^-1 \in coef0_eq1.
+Proof. by move=> hf; rewrite rpredVr. Qed.
+
+Lemma coef0_eq1_div f g :
+  f \in coef0_eq1 -> g \in coef0_eq1 -> f / g \in coef0_eq1.
+Proof. by move=> hf hg; rewrite rpred_div. Qed.
+
+Lemma coef0_eq1_unit f : f \in coef0_eq1 -> f \is a GRing.unit.
+Proof. by rewrite !coef0_eq1E unit_tfpsE => /eqP ->; apply unitr1. Qed.
+
+End Coefficient01Unit.
+
+
+Section Coefficient01IDomain.
+
+Variables (R : idomainType) (n : nat).
+Implicit Types (f g : {tfps R n}).
+
+Fact coef0_eq0_prime : prime_idealr_closed (@coef0_eq0 R n).
+Proof.
+by move => x y; rewrite -!topredE /= /coef0_eq0 coef0_tfpsM mulf_eq0.
+Qed.
+Canonical coef0_eq0_pideal :=
+  MkPrimeIdeal (coef0_eq0_ideal R n) coef0_eq0_prime.
+
+Example coef0_eq0_prime_test f g :
+  f * g \in coef0_eq0 -> (f \in coef0_eq0) || (g \in coef0_eq0).
 Proof. by rewrite prime_idealrM. Qed.
 
-Fact mulr_closed_c0_is_1 : mulr_closed coef0_is_1.
+End Coefficient01IDomain.
+
+
+Section MoreExpPoly.
+
+Variable (R : ringType).
+Implicit Type (p q : {poly R}).
+
+Lemma coefX_eq0 n m p : p`_0 = 0 -> n < m -> (p ^+ m)`_n = 0.
+Proof.
+elim: m n p => [|m IHm] n p Hp; first by rewrite ltn0.
+case: n => [_|n].
+  suff -> : (p ^+ m.+1)`_0 = (p`_0) ^+ m.+1 by rewrite Hp expr0n.
+  elim: m.+1 {IHm} => {m}[|m IHm]; first by rewrite !expr0 coef1 eq_refl.
+  by rewrite !exprS -{}IHm coefM big_ord_recl big_ord0 addr0.
+rewrite ltnS exprS => lt_nm.
+rewrite coefM; apply big1 => [] [j]; rewrite /= ltnS => le_ji _.
+case: j le_ji => [|j]; first by rewrite Hp mul0r.
+rewrite !ltnS subSS => le_jn.
+by rewrite IHm ?mulr0 // (leq_ltn_trans (leq_subr _ _ ) lt_nm).
+Qed.
+
+Lemma trXnX_eq0 n m p : p`_0 = 0 -> n < m -> trXn n (p ^+ m) = 0.
+Proof.
+move=> H1 H2.
+apply/tfpsP => i le_in; rewrite coef_trXn coef0 le_in.
+by rewrite coefX_eq0 // (leq_ltn_trans le_in H2).
+Qed.
+
+Lemma trXnMX_eq0 n p q i j :
+  p`_0 = 0 -> q`_0 = 0 -> n < i + j -> trXn n (p ^+ i * q ^+ j) = 0.
+Proof.
+move=> p0 q0 lt_n_addij.
+apply/tfpsP => l le_li; rewrite coef0.
+rewrite coef_trXn le_li coefM.
+rewrite (bigID (fun k => val k >= i)) /= ?big1 ?addr0 // => [] [k Hk] /= H.
+- rewrite -ltnNge in H.
+  by rewrite coefX_eq0 ?mul0r.
+- rewrite ltnS in Hk.
+  rewrite [X in _* X]coefX_eq0 ?mulr0 //.
+  rewrite leq_ltn_subLR //.
+  exact: (leq_ltn_trans le_li (leq_trans lt_n_addij (leq_add _ _))).
+Qed.
+
+Lemma coefX_tfps_eq0 n m i :
+  i < m -> {in coef0_eq0, forall f : {tfps R n}, (f ^+ m)`_i = 0}.
+Proof.
+move=> lt_im f; rewrite coef0_eq0E => /eqP/coefX_eq0/(_ lt_im).
+by rewrite coef_tfpsE !exp_tfps_val coef_trXn => ->; rewrite if_same.
+Qed.
+
+Lemma tfpsX_eq0 (n m : nat) :
+  n < m -> {in coef0_eq0, forall f : {tfps R n}, f ^+ m = 0}.
+Proof.
+move=> le_nm f /coefX_tfps_eq0 H0.
+apply/tfpsP => i le_in.
+by rewrite coef_tfps0 H0 // (leq_ltn_trans le_in le_nm).
+Qed.
+
+Lemma tfpsMX_eq0 n i j : n < i + j ->
+  {in @coef0_eq0 R n &, forall f g, f ^+ i * g ^+ j = 0}.
+Proof.
+move=> lt_n_addij f g f0 g0.
+apply tfps_inj.
+rewrite mul_tfps_val !exp_tfps_val trXn_mul.
+by rewrite trXnMX_eq0 //= -/(_`_0) ?(eqP f0) ?(eqP g0).
+Qed.
+
+End MoreExpPoly.
+
+
+Section GeometricSeries.
+
+Variables (R : ringType) (n : nat).
+Implicit Types (f g : {tfps R n}).
+
+Lemma geometricMl f :
+  f \in coef0_eq0 -> (1 - f) * (\sum_(i < n.+1) f ^+ i) = 1.
+Proof.
+move=> f0_eq0.
+have:= telescope_sumr (fun i => f ^+ i) (leq0n n.+1).
+rewrite big_mkord expr0 tfpsX_eq0 // sub0r => /(congr1 (fun x => -x)).
+rewrite opprK => {2}<-.
+rewrite mulr_sumr -sumrN; apply eq_bigr => /= i _.
+by rewrite opprB mulrBl mul1r -exprS.
+Qed.
+
+Lemma geometricMr f :
+  f \in coef0_eq0 -> (\sum_(i < n.+1) f ^+ i) * (1 - f) = 1.
+Proof.
+move=> /geometricMl {2}<-; apply/commr_sym/commr_sum => i _.
+apply/commr_sym/commrB; do [exact:commr1 |].
+by apply/commr_sym/commrX.
+Qed.
+
+End GeometricSeries.
+
+
+Section GeometricSeriesUnit.
+
+Variables (R : unitRingType) (n : nat).
+Implicit Types (c : R) (f g : {tfps R n}).
+
+Lemma geometricV f :
+  f \in coef0_eq0 -> (1 - f) ^-1 = \sum_(i < n.+1) f ^+ i.
+Proof.
+move=> f0_eq0.
+have f1unit : 1 - f \is a GRing.unit.
+  by apply: coef0_eq1_unit; rewrite -coef0_eq01 rpredN.
+by apply: (mulrI f1unit); rewrite geometricMl // divrr.
+Qed.
+
+Lemma geometric_1cNV c :
+  (1 - c *: \Xo(n))^-1 = \sum_(i < n.+1) (c *: \X) ^+ i.
+Proof. exact/geometricV/coef0_eq0Z/tfpsX_in_coef0_eq0. Qed.
+
+Lemma coeff_geometric_1cNV c m :
+  m <= n -> ((1 - c *: \Xo(n))^-1)`_m = c ^+ m.
+Proof.
+rewrite geometric_1cNV coeft_sum -ltnS => lt_mn1.
+rewrite (bigD1 (Ordinal lt_mn1)) //=.
+rewrite expr_cX coeftZ coef_tfpsXn -ltnS lt_mn1 eqxx mulr1 big1 ?addr0 // => i.
+rewrite -val_eqE /= => /negbTE eq_imF.
+by rewrite expr_cX coeftZ coef_tfpsXn eq_sym eq_imF andbF mulr0.
+Qed.
+
+Lemma coeff_geometric_1cV c m :
+  m <= n -> ((1 + c *: \Xo(n))^-1)`_m = (-c) ^+ m.
+Proof. by rewrite -{1}[c]opprK scaleNr; apply: coeff_geometric_1cNV. Qed.
+
+End GeometricSeriesUnit.
+
+
+Section DivisionByX.
+
+Variable R : ringType.
+
+Definition mulfX m (f : {tfps R m}) :=
+  [tfps i <= m.+1 => if i == 0%N then 0 else f`_i.-1].
+Definition divfX m (f : {tfps R m}) :=
+  [tfps i <= m.-1 => f`_i.+1].
+
+Lemma coef_mulfX m (f : {tfps R m}) i :
+  (mulfX f)`_i = if i == 0%N then 0 else f`_i.-1.
+Proof.
+rewrite coef_tfps_of_fun; case: i => //= i.
+rewrite ltnS; case: leqP => // lt_mi.
+by rewrite nth_default // (leq_trans (size_tfps f) lt_mi).
+Qed.
+Lemma coef_divfX m (f : {tfps R m}) i : (divfX f)`_i = f`_i.+1.
+Proof.
+rewrite coef_tfps_of_fun; case: leqP => // Hi.
+rewrite nth_default // (leq_trans (size_tfps f)) //.
+by move: Hi; case m.
+Qed.
+
+Lemma mulfXK m : cancel (@mulfX m) (@divfX m.+1).
+Proof.
+move=> p; apply/tfpsP => i Hi.
+by rewrite coef_divfX coef_mulfX.
+Qed.
+
+Lemma divfXK m : {in coef0_eq0, cancel (@divfX m.+1) (@mulfX m)}.
+Proof.
+move=> p Hp.
+by apply/tfpsP => [[|i]] Hi; rewrite coef_mulfX coef_divfX // (eqP Hp).
+Qed.
+
+Lemma mulfX1 m : mulfX 1 = \X :> {tfps R m.+1}.
+Proof.
+by apply/tfpsP => [] [|[|i]] _;
+  rewrite coef_mulfX coef_tfpsX // ?coef_tfps1 ?mulr1 ?mulr0.
+Qed.
+Lemma divfXX m : divfX (\X : {tfps R m.+1}) = 1 :> {tfps R m}.
+Proof. by rewrite -[RHS]mulfXK mulfX1. Qed.
+
+Fact mulfX_is_linear m : linear (@mulfX m).
+Proof.
+move=> c f g; apply/tfpsP => i _; rewrite !(coeftD, coeftZ, coef_mulfX).
+by case: eqP => //; rewrite mulr0 add0r.
+Qed.
+Canonical mulfX_additive m := Additive (@mulfX_is_linear m).
+Canonical mulfX_linear m := Linear (@mulfX_is_linear m).
+
+Fact divfX_is_linear m : linear (@divfX m).
+Proof.
+by move=> c f g; apply/tfpsP => i _; rewrite !(coeftD, coeftZ, coef_divfX).
+Qed.
+Canonical divfX_additive m := Additive (@divfX_is_linear m).
+Canonical divfX_linear m := Linear (@divfX_is_linear m).
+
+
+Variable m : nat.
+Implicit Type f : {tfps R m}.
+
+Lemma trXn_mulfXE f : trXn m (tfps (mulfX f)) = \X * f.
+Proof.
+apply/tfpsP => i Hi.
+by rewrite coef_trXn coef_mulfX coef_tfpsXM Hi.
+Qed.
+
+Lemma mulfXE f : mulfX f = \X * trXnt m.+1 f.
+Proof.
+apply/tfpsP => i Hi.
+rewrite coef_mulfX coef_tfpsXM coef_trXnt Hi.
+by case: i Hi => //= i /ltnW ->.
+Qed.
+
+Lemma trXnt_mulfX f n :
+  n <= m -> trXnt n.+1 (mulfX f) = mulfX (trXnt n f).
+Proof.
+move=> le_nm; apply/tfpsP => i le_in1.
+rewrite coef_trXnt !coef_mulfX le_in1.
+by case: i le_in1 => //= i; rewrite ltnS coef_trXnt => ->.
+Qed.
+
+Lemma mulfXM f (g : {tfps R m.+1}) : (mulfX f) * g = mulfX (f * trXnt m g).
+Proof.
+apply/tfpsP => [[|i]].
+  by rewrite !(coef0_tfpsM, coef_mulfX, coef0_trXn, coef_tfpsE) /= mul0r.
+rewrite ltnS => le_im.
+rewrite coef_mulfX /= -/(_`_i.+1) !coefM_tfps ltnS le_im.
+rewrite big_ord_recl /= -/(_`_0) coef_mulfX /= mul0r add0r.
+apply eq_bigr => [[j] /=]; rewrite ltnS => le_ji _.
+rewrite -/(_`_j.+1) coef_mulfX /= /bump /= add1n subSS.
+by rewrite coef_trXnt (leq_trans (leq_subr _ _) le_im).
+Qed.
+
+Lemma coef_mulfX_exp_lt f i j : i < j -> (mulfX f ^+ j)`_i = 0.
+Proof.
+elim: j i => [|j IHj] i //; rewrite ltnS => le_ij.
+rewrite exprS coefM_tfps; case leqP => // _.
+rewrite big_ord_recl big1 ?coef_mulfX ?mul0r ?add0r // => [[u /=]] lt_ui _.
+rewrite {}IHj ?mulr0 // /bump /= add1n.
+case: i lt_ui le_ij => // i _ lt_ij.
+by rewrite subSS (leq_ltn_trans (leq_subr _ _) lt_ij).
+Qed.
+
+Lemma coef_mulfX_exp f i : i <= m.+1 -> (mulfX f ^+ i)`_i = (f ^+ i)`_0.
+Proof.
+elim: i => [|i IHi] lt_im1; first by rewrite !expr0 coef1.
+rewrite exprS coefM_tfps (leq_trans lt_im1 _) //.
+rewrite big_ord_recl coef_mulfX mul0r add0r.
+rewrite big_ord_recl coef_mulfX /= /bump /= add1n subSS subn0.
+rewrite {}IHi ?(ltnW lt_im1) // -!/(_`_0).
+rewrite -coef0_tfpsM ?rpredX // -exprS.
+rewrite big1 ?addr0 // => [[j /= lt_ji]] _.
+rewrite !add1n subSS coef_mulfX_exp_lt ?mulr0 //.
+case: i lt_ji {lt_im1} => // i.
+by rewrite !ltnS subSS leq_subr.
+Qed.
+
+End DivisionByX.
+
+Lemma divfXE (K : idomainType) m :
+  {in @coef0_eq0 K m, forall f, divfX f = trXn m.-1 (tfps f %/ 'X)}.
+Proof.
+move=> f.
+move/eqP/polyXP; rewrite Pdiv.IdomainUnit.dvdp_eq ?lead_coefX ?unitr1 //.
+rewrite /divfX; move/eqP => h; apply/tfpsP => i Hi.
+by rewrite coef_poly coef_trXn ltnS Hi coef_tfpsE [in LHS]h coefMX.
+Qed.
+
+
+Section MapMulfXDivfX.
+
+Variables (K L : ringType) (F : {rmorphism K -> L}) (m : nat) (g : {tfps K m}).
+
+Lemma map_tfps_mulfX : map_tfps F (mulfX g) = mulfX (map_tfps F g).
+Proof.
+apply/tfpsP => i lt_im1.
+rewrite !(coef_mulfX, coef_map, lt_im1).
+by case: i {lt_im1}=> [|j]//=; rewrite rmorph0.
+Qed.
+
+Lemma map_tfps_divfX : map_tfps F (divfX g) = divfX (map_tfps F g).
+Proof.
+apply/tfpsP => i lt_im1.
+by rewrite !(coef_divfX, coef_map, lt_im1).
+Qed.
+
+End MapMulfXDivfX.
+
+
+Section Derivative.
+
+Variables (R : ringType) (n : nat).
+Implicit Types (f g : {tfps R n}).
+
+Lemma deriv_trXn (p : {poly R}) :
+  (tfps (trXn n.+1 p))^`() = tfps (trXn n (p^`())).
+Proof.
+apply/polyP => i /=.
+rewrite coef_deriv !coef_trXn coef_deriv ltnS.
+by case: leqP => //; rewrite mul0rn.
+Qed.
+
+Fact trXn_deriv (m : nat) (f : {tfps R n}) : n <= m ->
+  tfps (trXn m (tfps f)^`()) = (tfps f)^`().
+Proof.
+move => le_nm; apply/polyP => i /=.
+rewrite coef_deriv !coef_trXn coef_deriv.
+case: leqP => lt_mi //.
+by rewrite coef_tfps (leq_gtF (ltnW (leq_ltn_trans le_nm lt_mi))) mul0rn.
+Qed.
+
+Definition deriv_tfps f := [tfps j <= n.-1 => f`_j.+1 *+ j.+1].
+Local Notation "f ^` () " := (deriv_tfps f) : tfps_scope.
+
+Lemma coef_deriv_tfps f j : (deriv_tfps f)`_j = f`_j.+1 *+ j.+1.
+Proof.
+rewrite coef_tfps_of_fun; case: leqP => //.
+rewrite coef_tfps [j < n]ltnNge.
+by case: n f => /= [|m f ->]; rewrite mul0rn.
+Qed.
+
+Lemma val_deriv_tfps f : tfps (deriv_tfps f) = (tfps f)^`()%R.
+Proof. by apply/polyP => i; rewrite coef_deriv_tfps coef_deriv. Qed.
+
+Lemma deriv_tfpsE f : deriv_tfps f = trXn n.-1 (tfps f)^`().
+Proof. by rewrite -val_deriv_tfps tfpsK. Qed.
+
+Fact deriv_tfps0 : (0 : {tfps R n})^`() = 0.
+Proof. by apply tfps_inj; rewrite val_deriv_tfps deriv0. Qed.
+
+Lemma deriv_tfpsC (c : R) : c%:S^`() = 0.
+Proof. by apply tfps_inj; rewrite val_deriv_tfps /= val_tfpsC derivC. Qed.
+
+Lemma deriv_tfps1 : 1^`() = 0.
+Proof. by rewrite -tfpsC1 deriv_tfpsC. Qed.
+
+Fact deriv_tfpsD f g : (f + g)^`() = f^`()%tfps + g^`()%tfps.
+Proof.
+apply/tfpsP => i le_in1.
+by rewrite coefD !coef_poly ltnS le_in1 coefD -mulrnDl.
+Qed.
+
+Fact deriv_tfpsZ (c : R) f : (c *: f)^`() = c *: f^`()%tfps.
+Proof.
+apply/tfpsP => i le_in1.
+by rewrite !(coef_poly, coefZ) ltnS le_in1 mulrnAr.
+Qed.
+
+Fact deriv_tfps_is_linear : linear deriv_tfps.
+Proof. by move => c f g; rewrite deriv_tfpsD deriv_tfpsZ. Qed.
+Canonical deriv_tfps_additive := Additive deriv_tfps_is_linear.
+Canonical deriv_tfps_linear := Linear deriv_tfps_is_linear.
+
+(* Tests *)
+Example test_deriv_tfps0 : 0^`() = 0.
+Proof. by rewrite linear0. Qed.
+
+Example test_deriv_tfpsD f g : (f + g)^`() = f^`()%tfps + g^`()%tfps.
+Proof. by rewrite linearD. Qed.
+
+End Derivative.
+
+Notation "f ^` () " := (deriv_tfps f) : tfps_scope.
+
+
+Section MoreDerivative.
+
+Variables (R : ringType).
+
+Lemma deriv_tfpsX n : \Xo(n.+1)^`() = 1  :> {tfps R n}.
+Proof. by rewrite deriv_tfpsE val_tfpsX scale1r derivX trXn1. Qed.
+
+Lemma deriv_trXnt m n (p : {tfps R m}) :
+  (trXnt n.+1 p)^`()%tfps = trXnt n p^`()%tfps.
+Proof.
+rewrite /trXnt deriv_tfpsE deriv_trXn [n.+1.-1]/= trXn_trXn //.
+by rewrite -val_deriv_tfps.
+Qed.
+
+Lemma deriv_tfps0p (f : {tfps R 0}) : f^`() = 0.
+Proof. by rewrite [f]tfps_is_cst deriv_tfpsC. Qed.
+
+Theorem derivM_tfps n (f g : {tfps R n}) :
+  (f * g)^`() = f^`()%tfps * (trXnt n.-1 g) + (trXnt n.-1 f) * g^`()%tfps.
+Proof.
+move: f g; case: n => /= [f g | m f g].
+  rewrite [f]tfps_is_cst [g]tfps_is_cst -tfpsCM !deriv_tfpsC.
+  by rewrite mul0r mulr0 addr0.
+apply/tfps_inj; rewrite !deriv_tfpsE deriv_trXn /=.
+by rewrite trXn_trXn // derivM rmorphD !rmorphM.
+Qed.
+
+(* Noncommutative version *)
+Theorem derivX_tfps_nc n (f : {tfps R n}) k :
+  (f ^+ k)^`() =
+  \sum_(i < k) (trXnt n.-1 f) ^+ i * f^`()%tfps * (trXnt n.-1 f) ^+ (k.-1 - i).
+Proof.
+have Hn := leq_pred n.
+case: k; first by rewrite !expr0 deriv_tfps1 big_ord0.
+elim=> [|k IHk] /=.
+  by rewrite !expr1 big_ord_recl big_ord0 addr0 subnn expr0 mul1r mulr1.
+rewrite exprS derivM_tfps big_ord_recl subn0 expr0 mul1r rmorphX /=.
+congr (_ + _).
+rewrite {}IHk mulr_sumr; apply eq_bigr => i _.
+by rewrite /bump /= add1n subSS !mulrA -exprS.
+Qed.
+
+End MoreDerivative.
+
+
+Section DerivativeComRing.
+
+Variables (R : comRingType) (n : nat).
+Implicit Types (f g : {tfps R n}).
+
+
+Theorem derivX_tfps f k :
+  (f ^+ k)^`() = (trXnt n.-1 f) ^+ k.-1 * f^`()%tfps *+ k.
+Proof.
+have Hn := leq_pred n.
+rewrite derivX_tfps_nc -{9}(card_ord k) -sumr_const.
+apply eq_bigr => [] [i /= Hi] _.
+by rewrite mulrC mulrA -!rmorphX -rmorphM /= -exprD subnK //; case: k Hi.
+Qed.
+
+Theorem derivX_tfps_bis f k :
+  (f ^+ k)^`() = f^`()%tfps * (trXnt n.-1 f) ^+ (k.-1) *+ k.
+Proof. by rewrite derivX_tfps mulrC. Qed.
+
+End DerivativeComRing.
+
+
+Section DerivativeUnitRing.
+
+Variables (R : unitRingType) (n : nat).
+Implicit Types (f g : {tfps R n}).
+
+(* Noncommutative version *)
+Theorem derivV_tfps_nc f :
+  f \is a GRing.unit ->
+  (f ^-1)^`() = - trXnt n.-1 (f^-1) * f^`()%tfps * trXnt n.-1 (f^-1).
+Proof.
+move => fU.
+have:= erefl (f / f); rewrite {2}divrr //.
+move/(congr1 (@deriv_tfps R n)).
+rewrite derivM_tfps -tfpsC1 deriv_tfpsC.
+(* Coq is confused with the pattern matching :-( ?? Let's help him ! *)
+move/eqP; rewrite addrC; set X := (X in X + _); rewrite (addr_eq0 X _) {}/X.
+move/eqP/(congr1 (fun x => (trXnt n.-1 f ^-1) * x)).
+rewrite {1}trXntV ?leq_pred // mulKr ?(mulrN, mulNr, mulrA) //.
+by rewrite unit_tfpsE coef0_trXn.
+Qed.
+
+End DerivativeUnitRing.
+
+
+Section DerivativeComUnitRing.
+
+Variables (R : comUnitRingType) (n : nat).
+Implicit Types (f g : {tfps R n}).
+
+Theorem derivV_tfps f :
+  f \is a GRing.unit -> (f ^-1)^`() = - f^`()%tfps / trXnt n.-1 (f ^+ 2).
+Proof.
+move=> fU.
+rewrite derivV_tfps_nc // -mulrA mulrC -mulrA !mulrN mulNr.
+rewrite trXntV ?leq_pred // -invrM ?unit_tfpsE ?coef0_trXn //.
+by rewrite -{1}rmorphM ?leq_pred.
+Qed.
+
+Theorem deriv_div_tfps f g :
+  g \is a GRing.unit ->
+  (f / g)^`() = (f^`()%tfps * trXnt n.-1 g - trXnt n.-1 f * g^`()%tfps)
+                                                    / (trXnt n.-1 (g ^+ 2)).
+Proof.
+move => fU.
+rewrite derivM_tfps derivV_tfps // mulrBl mulrA mulrN mulNr.
+congr (_ - _); rewrite -mulrA; congr (_ * _).
+rewrite trXntV ?leq_pred // expr2 ?leq_pred //.
+rewrite rmorphM ?leq_pred //= => Hn.
+by rewrite invrM ?mulrA ?divrr ?div1r // trXnt_unitE.
+Qed.
+
+End DerivativeComUnitRing.
+
+
+Section Primitive.
+
+Variables (R : unitRingType) (n : nat).
+
+Definition prim (p : {poly R}) :=
+  \poly_(i < (size p).+1) (p`_i.-1 *+ (i != 0%N) / (i%:R)).
+
+Local Notation "\int p" := (prim p) (at level 2).
+
+Lemma coef_prim (p : {poly R}) (i : nat) :
+  (\int p)`_i = if i == 0%N then 0 else p`_i.-1 / (i%:R).
+Proof.
+case: i => [| i]; first by rewrite eqxx coef_poly invr0 mulr0.
+rewrite succnK eqn0Ngt ltn0Sn coef_poly.
+rewrite eqn0Ngt ltn0Sn /= -{3}[p]coefK coef_poly ltnS.
+by case: (i < size p) => //; rewrite mul0r.
+Qed.
+
+Lemma coef0_prim (p : {poly R}) : (\int p)`_0 = 0.
+Proof. by rewrite coef_prim eqxx. Qed.
+
+Lemma primC (c : R) : \int (c%:P) = c *: 'X.
+Proof.
+apply/polyP => i.
+rewrite /prim /prim coef_poly size_polyC -[c *: 'X]coefK.
+have [-> | c_neq0 ] := eqVneq c 0.
+  rewrite eqxx /= scale0r size_poly0 coef_poly ltn0; case: i => [|i].
+    by rewrite invr0 mulr0.
+    by rewrite coefC.
+rewrite c_neq0 /= coef_poly coefZ coefX.
+have -> : size (c *: 'X) = 2%N.
+  rewrite -mulr_algl alg_polyC size_Mmonic ?monicX ?polyC_eq0 //.
+  by rewrite size_polyX size_polyC c_neq0.
+congr if_expr; case: i => [|i]; first by rewrite invr0 !mulr0.
+rewrite coefC mulr1n.
+case: i => [|i]; first by rewrite !eqxx invr1.
+by rewrite /= mul0r mulr0.
+Qed.
+
+Lemma primX : \int 'X = (2%:R) ^-1 *: 'X ^+2.
+Proof.
+rewrite /prim /prim size_polyX ; apply/polyP => i.
+rewrite coef_poly coefZ coefXn coefX.
+case: i => [|i]; first by rewrite invr0 !mulr0.
+rewrite eqn0Ngt ltn0Sn /=; case: i => [ | i ] ; first by rewrite mul0r mulr0.
+case: i => [|i]; first by rewrite mul1r mulr1.
+by rewrite mulr0.
+Qed.
+
+Lemma primXn (m : nat): \int ('X ^+ m) = (m.+1 %:R) ^-1 *: 'X ^+ m.+1.
+Proof.
+rewrite /prim /prim size_polyXn ; apply/polyP => i.
+rewrite coefZ !coefXn coef_poly !coefXn.
+have [-> | /negbTE i_neq_Sm ] := eqVneq i m.+1.
+  by rewrite eqxx ltnSn mulr1 eqxx mul1r.
+rewrite i_neq_Sm /= mulr0 ; case: (i < m.+2) => [] //.
+have [ -> | /negbTE i_neq0 ] := eqVneq i 0%N; first by rewrite eqxx invr0 mulr0.
+rewrite i_neq0 ; move/negbT : i_neq0 ; move/negbT : i_neq_Sm.
+case: i => [ // | i ].
+by rewrite (inj_eq succn_inj) => /negbTE -> _ ; rewrite mul0r.
+Qed.
+
+Fact prim_is_linear : linear prim.
+Proof.
+move => k p q ; apply/polyP => i.
+case: i => [ | i]; first by rewrite coefD coefZ !coef0_prim mulr0 addr0.
+by rewrite !(coef_prim, coefD, coefZ) mulrDl -mulrA.
+Qed.
+Canonical prim_additive := Additive prim_is_linear.
+Canonical prim_linear := Linear prim_is_linear.
+
+(* tests *)
+Fact prim0 : prim 0 = 0.
+Proof. exact: linear0. Qed.
+
+Fact primD : {morph prim : p q / p + q}.
+Proof. exact: linearD. Qed.
+
+Fact primN : {morph prim : p / - p}.
+Proof. exact: linearN. Qed.
+
+Fact primB : {morph prim : p q / p - q}.
+Proof. exact: linearB. Qed.
+
+
+Implicit Types (f g : {tfps R n}).
+
+Lemma size_prim_leq f : size (prim (tfps f)) <= n.+2.
+Proof.
+apply: (leq_trans (size_poly _ _) _); rewrite ltnS.
+exact: size_tfps.
+Qed.
+Definition prim_tfps f := Tfps_of (size_prim_leq f).
+
+Lemma coef_prim_tfps f i : (prim_tfps f)`_i = (prim (tfps f))`_i.
+Proof. by []. Qed.
+
+Fact prim_tfps_is_linear : linear prim_tfps.
+Proof.
+move=> k p q; apply/tfpsP => i lt_in1.
+rewrite coefD coefZ !coef_prim.
+case: i lt_in1 => [|i]/=; first by rewrite mulr0 addr0.
+rewrite ltnS => lt_in.
+by rewrite coefD coefZ mulrDl mulrA.
+Qed.
+Canonical prim_tfps_additive := Additive prim_tfps_is_linear.
+Canonical prim_tfps_linear := Linear prim_tfps_is_linear.
+
+(* tests *)
+Example prim_tfps0 : prim_tfps 0 = 0.
+Proof. exact: linear0. Qed.
+
+Example prim_tfpsD : {morph prim_tfps : p q / p + q}.
+Proof. exact: linearD. Qed.
+
+Lemma coef0_prim_tfps f : (prim_tfps f)`_0 = 0.
+Proof. by rewrite coef_poly eqxx mulr0n invr0 mulr0. Qed.
+
+End Primitive.
+
+
+Section MoreCompPoly.
+
+Variable (R : ringType).
+Implicit Type (p q : {poly R}).
+
+Lemma trXn_comp_polyr n p q :
+  trXn n (p \Po q) = trXn n (p \Po (tfps (trXn n q))).
 Proof.
-split=> [|x y]; rewrite !coef0_is_1E ?coefC //. 
-by rewrite nth0_mul_tfps; move/eqP ->; move/eqP ->; rewrite mul1r.
+apply/trXnP => i le_in.
+rewrite !coef_comp_poly; apply eq_bigr => j _; congr (_ * _).
+have /= := (congr1 (fun x => (tfps x)`_i) (exp_tfps_val (trXn n q) j)).
+rewrite !coef_trXn le_in => <-.
+by rewrite -rmorphX coef_trXn le_in.
 Qed.
 
-Fact invr_closed_c0_is_1 : invr_closed coef0_is_1.
-Proof. 
-move=> f; rewrite !coef0_is_1E nth0_inv; move/eqP ->. 
-by rewrite invr1.
+Lemma trXn_comp_polyl n p q :
+  q`_0 = 0 -> trXn n (p \Po q) = trXn n ((tfps (trXn n p)) \Po q).
+Proof.
+move => q0_eq0; apply/trXnP => i le_in.
+rewrite -{1}(poly_cat p n.+1) comp_polyD coefD !trXnE.
+rewrite [X in _ + X](_ : _ = 0) ?addr0 //.
+rewrite coef_comp_poly; apply big1 => [] [j /=] le_jsz _.
+rewrite coefXnM; case: ltnP => [] Hi; first by rewrite mul0r.
+by rewrite coefX_eq0 ?mulr0 // (leq_ltn_trans le_in Hi).
 Qed.
 
-Fact c0_is_1_key : pred_key coef0_is_1. Proof. by []. Qed.
+End MoreCompPoly.
 
-Canonical c0_is_1_keyed := KeyedPred c0_is_1_key.
 
-Canonical c0_is_1_MulrPred := MulrPred mulr_closed_c0_is_1.
-Canonical c0_is_1_DivrPred := DivrPred invr_closed_c0_is_1.
+Section Composition.
 
-(* tests *)
-Example one_in_coef0_is_1 : 1 \in coef0_is_1.
-Proof. by rewrite rpred1. Qed.
+Variables (R : ringType) (n : nat).
 
-Example coef0_is_1M f g :
-    f \in coef0_is_1 -> g \in coef0_is_1 -> f * g \in coef0_is_1.
-Proof. by move=> hf hg; rewrite rpredM. Qed.
+Definition comp_tfps m (f g : {tfps R m}) :=
+  if f \in coef0_eq0
+  then trXn m (tfps g \Po tfps f)
+  else (g`_0%N)%:S.  (* avoid particular cases (e.g. associatvity) *)
 
-Example coef0_is_1V f : f \in coef0_is_1 -> f^-1 \in coef0_is_1.
-Proof. by move=> hf; rewrite rpredVr. Qed.
+Local Notation "f \So g" := (comp_tfps g f) : tfps_scope.
 
-Example coef0_is_1_div f g : 
-    f \in coef0_is_1 -> g \in coef0_is_1 -> f / g \in coef0_is_1.
-Proof. by move=> hf hg; rewrite rpred_div. Qed.
 
-End Coefficient01.
+Lemma comp_tfps_coef0_neq0 m (f g : {tfps R m}) :
+  g \notin coef0_eq0 -> f \So g = (f`_0%N)%:S.
+Proof. by move/negbTE => p0_neq0; rewrite /comp_tfps p0_neq0. Qed.
 
-Section DivisionByX.
+Lemma comp_tfps_coef0_eq0 m (f g : {tfps R m}) :
+  g \in coef0_eq0 -> f \So g = trXn m (tfps f \Po tfps g).
+Proof. by move => f0_eq0 ; rewrite /comp_tfps f0_eq0. Qed.
+
+Lemma comp_tfps0r m (f : {tfps R m}) : f \So 0 = (f`_0)%:S.
+Proof.
+rewrite comp_tfps_coef0_eq0 ?rpred0 // comp_poly0r.
+by rewrite -tfpsCE -coef_tfpsE.
+Qed.
 
-Variable (K : fieldType).
+Lemma comp_tfps0l m (f : {tfps R m}) : 0 \So f = 0.
+Proof.
+case (boolP (f \in coef0_eq0)) => [f0_eq0 | f0_neq0].
+- by rewrite comp_tfps_coef0_eq0 // comp_poly0 rmorph0.
+- by rewrite comp_tfps_coef0_neq0 // coef_tfps0 tfpsC0.
+Qed.
 
-Definition divfX (m : nat) (f : {tfps K m}) := Tfpsp m.-1 (f %/ 'X).
+Implicit Types (f g h : {tfps R n}) (p q : {poly R}).
 
-Lemma divfXE (m : nat) (f : {tfps K m}) : 
-  f \in (@coef0_is_0 K m) -> divfX f = [tfps i => f`_i.+1].
+Lemma coef0_comp_tfps f g : (f \So g)`_0 = f`_0.
 Proof.
-move/eqP/polyXP; rewrite dvdp_eq /divfX; move/eqP => h.
-rewrite [in RHS]h; apply/eq_tfps => i.
-by rewrite coef_poly coef_modXn coefMX.
-Qed. 
+rewrite /comp_tfps; case: (boolP (_ \in _)); last by rewrite coef_tfpsC.
+rewrite coef0_eq0E coef_trXn {-2}[0%N]lock /= -lock => /eqP g0_eq0.
+rewrite coef_comp_poly.
+case Hsz : (size (tfps f)) => [|sz].
+  by rewrite big_ord0 nth_default // leqn0 size_tfpsE Hsz.
+rewrite big_ord_recl big1.
+- by rewrite addr0 -coef_tfpsE expr0 coef1 mulr1.
+- move=> [i /= Hi] _.
+  by rewrite /bump /= -/(_`_0) add1n exprSr coef0M -coef_tfpsE g0_eq0 !mulr0.
+Qed.
 
-End DivisionByX.
+Lemma coef_comp_tfps k f g :
+  g \in coef0_eq0 -> (f \So g)`_k = \sum_(i < k.+1) f`_i * (g ^+ i)`_k.
+Proof.
+move=> g0; rewrite (comp_tfps_coef0_eq0 _ g0).
+rewrite coef_trXn; case: leqP => [le_kn | lt_nk].
+- rewrite coef_comp_poly.
+  have co_is0 i : minn (size f) k.+1 <= i -> f`_i * (g ^+ i)`_k = 0.
+    rewrite geq_min => /orP [/(nth_default _) ->| lt_ki]; first by rewrite mul0r.
+    rewrite !coef_tfpsE !exp_tfps_val coef_trXn le_kn.
+    by rewrite coefX_eq0 ?mulr0 ?(eqP g0).
+  rewrite [RHS](bigID (fun i : 'I_ _ => i < minn (size f) k.+1)) /=.
+  rewrite [LHS](bigID (fun i : 'I_ _ => i < minn (size f) k.+1)) /=.
+  rewrite [X in _ + X]big1 ?addr0; first last.
+    move=> [i /=] _; rewrite -leqNgt => /co_is0 /=.
+    by rewrite !coef_tfpsE !exp_tfps_val coef_trXn le_kn.
+  rewrite [X in _ + X]big1 ?addr0; first last.
+    by move=> [i /=] _; rewrite -leqNgt => /co_is0.
+  rewrite -(big_ord_widen _ (fun i => f`_i * (g ^+ i)`_k)) ?geq_minr //.
+  rewrite -(big_ord_widen _ (fun i => f`_i * (tfps g ^+ i)`_k)) ?geq_minl //.
+  by apply eq_bigr => i _; rewrite !coef_tfpsE !exp_tfps_val coef_trXn le_kn.
+- apply/esym/big1 => [[l /=]]; rewrite ltnS => Hl _.
+  by rewrite [_`_k]coef_tfps /= (ltn_geF lt_nk) mulr0.
+Qed.
 
-Lemma map_tfps_divfX (K L : fieldType) (f : {rmorphism K -> L})
-  (m : nat) (g : tfps K m) :
-  map_tfps f (divfX g) = divfX (map_tfps f g).
+Lemma trXnt_comp m f g :
+  m <= n -> trXnt m (f \So g) = (trXnt m f) \So (trXnt m g).
 Proof.
-apply/val_inj => /=.
-rewrite map_modp rmorphX /= map_polyX modp_mod map_divp map_polyX.
-by rewrite [(_ ^ _ %% _)]modp_small // size_polyXn size_map_poly ltnS size_tfps.
+case (boolP (g \in coef0_eq0)) => [g0_eq0 | g0_neq0] le_mn.
+- rewrite !comp_tfps_coef0_eq0 ?coef0_eq0_trXnt //.
+  rewrite /trXnt -trXn_comp_polyr -trXn_comp_polyl ?(eqP g0_eq0) //=.
+  by rewrite trXn_trXn.
+- rewrite !comp_tfps_coef0_neq0 ?coef0_eq0_trXnt //.
+  by rewrite trXntC coef_trXn.
 Qed.
 
-Section Derivative.
+Lemma coef0_eq0_comp f g : (f \So g \in coef0_eq0) = (f \in coef0_eq0).
+Proof. by rewrite !coef0_eq0E coef0_comp_tfps. Qed.
 
-Variables (K : fieldType) (n : nat).
+Lemma coef0_eq1_comp f g : (f \So g \in coef0_eq1) = (f \in coef0_eq1).
+Proof. by rewrite !coef0_eq1E coef0_comp_tfps. Qed.
 
-(* can be generalized with R ? *)
-Lemma deriv_modp (p : {poly K}) :
-    ((p %% 'X ^+ n.+1)^`() = (p ^`()) %% 'X ^+ n)%R.
+Lemma comp_tfpsC f (c : R) : c%:S \So f = c%:S.
 Proof.
-rewrite {2}[p](divp_eq _ ('X^n.+1)) derivD derivM !modp_add.
-rewrite -addrA [X in X + _]modp_eq0 ; last first.
-rewrite dvdp_mull // dvdp_Pexp2l ?leqnSn // size_polyX //.
-rewrite add0r [X in X + _]modp_eq0 ; last first.
-  rewrite dvdp_mull // derivXn /= -scaler_nat. 
-  have [->|Sm_neq0] := eqVneq (n.+1)%:R (0 : K).
-    by rewrite scale0r dvdp0.
-  by rewrite dvdp_scaler.
-rewrite add0r [RHS]modp_small // size_polyXn.
-have [-> | p_modXSm_neq0] := eqVneq (p %% 'X^n.+1) 0.
-+ by rewrite deriv0 size_poly0.
-+ by rewrite (leq_trans _ (leq_modpXn n.+1 p)) // lt_size_deriv.
+case (boolP (f \in coef0_eq0)) => [f0_eq0 | f0_neq0].
+- by rewrite comp_tfps_coef0_eq0 //= val_tfpsC comp_polyC -tfpsCE.
+- by rewrite comp_tfps_coef0_neq0 ?coef_tfpsC.
 Qed.
 
-Fact mod_deriv_tfps (m : nat) (f : {tfps K n}) : n <= m -> 
-  (val f)^`() %% 'X^m = ((val f)^`())%R.
+Lemma comp_tfps1 f : 1 \So f = 1.
+Proof. by rewrite -tfpsC1 comp_tfpsC. Qed.
+
+Lemma comp_tfpsCf f (c : R) : f \So (c%:S) = (f`_0)%:S.
 Proof.
-move => leq_nm; rewrite modp_small // size_polyXn ltnS.
-rewrite (leq_trans _ leq_nm) // (leq_trans (leq_size_deriv _)) //.
-have [->//|sfN0] := eqVneq (size (val f)) 0%N.
-by rewrite -ltnS prednK ?size_tfps // lt0n.
+have [->| c_neq0] := eqVneq c 0.
+  by rewrite tfpsC0 comp_tfps0r.
+by rewrite comp_tfps_coef0_neq0 // coef0_eq0E coef_tfpsC.
 Qed.
 
-Lemma deriv_tfpsE (f : {tfps K n}) : deriv_tfps f = Tfpsp n.-1 (val f)^`().
-Proof. 
-by apply/val_inj; apply/polyP => i; rewrite coef_poly coef_modXn coef_deriv. 
+Fact comp_tfps_is_linear (f : {tfps R n}) : linear (comp_tfps f).
+Proof.
+case: (boolP (f \in coef0_eq0)) => Hf a q r.
+- by rewrite !comp_tfps_coef0_eq0 // !raddfD /= !linearZ.
+- rewrite !comp_tfps_coef0_neq0 // coeftD coeftZ.
+  by rewrite raddfD /= -!/(_`_0) tfpsCM -alg_tfpsC mulr_algl.
 Qed.
+Canonical comp_tfps_additive f := Additive (comp_tfps_is_linear f).
+Canonical comp_tfps_linear f := Linear (comp_tfps_is_linear f).
 
-(* Local Notation "f ^` () " := (deriv_tfps f) (at level 8) : tfps_scope. *)
 
-Fact deriv_tfps0 : (0 : {tfps K n}) ^`() = 0.
+Lemma comp_tfpsXr f : f \So \X = f.
 Proof.
-apply/val_inj => /=; rewrite polyseq0; apply/polyP => i.
-by rewrite coef_poly coefC mul0rn; case: (_ < _); case: i. 
+case: n f => [|n'] f.
+  by rewrite tfps0X // comp_tfps0r {2}(tfps_is_cst f).
+rewrite comp_tfps_coef0_eq0 ?tfpsX_in_coef0_eq0 //.
+by rewrite val_tfpsSX comp_polyXr tfpsK.
 Qed.
 
-(* can I simplify this proof ? *)
-Lemma deriv_tfpsC (c : K) : c %:S ^`() = 0 :> {tfps _ n.-1}.
+Lemma comp_tfpsX : {in coef0_eq0, forall f, \X \So f = f}.
 Proof.
-apply/val_inj => /=; apply/polyP => i.
-rewrite modp_small; last first.
-  by rewrite size_polyC size_polyXn (leq_ltn_trans (leq_b1 _)).
-rewrite coef_poly coefC if_same polyseqC.
-by case: (_ < _) => //; case: (_ == _); rewrite /= ?nth_nil mul0rn.
-Qed. 
+case: n => [|n'] f.
+  rewrite tfps0X // comp_tfps0l {2}(tfps_is_cst f) => /eqP ->.
+  by rewrite tfpsC0.
+move=> /comp_tfps_coef0_eq0 ->.
+by rewrite val_tfpsSX comp_polyX tfpsK.
+Qed.
 
-Fact deriv_tfpsD (f g : {tfps K n}) : (f + g)^`() = f^`()%tfps + g^`()%tfps.
+Lemma comp_tfpsXn i : {in coef0_eq0, forall f, \X ^+ i \So f = f ^+ i}.
 Proof.
-apply/val_inj; apply/polyP => i; rewrite coefD !coef_poly coefD.
-by case: (_ < _) => //=; rewrite ?addr0 // -mulrnDl.
+move=> f Hf; apply/tfpsP => j Hj.
+rewrite coef_comp_tfps //.
+case: (ltnP i j.+1) => [lt_ij1 | lt_ji].
+- rewrite (bigD1 (Ordinal lt_ij1)) //= big1 ?addr0.
+  + rewrite ltnS in lt_ij1.
+    by rewrite coef_tfpsXn eqxx (leq_trans lt_ij1 Hj) mul1r.
+  + move=> [k Hk]; rewrite -val_eqE /= coef_tfpsXn => /negbTE ->.
+    by rewrite andbF mul0r.
+- rewrite coefX_tfps_eq0 // big1 // => [] [k /=]; rewrite ltnS => Hk _.
+  by rewrite coef_tfpsXn (ltn_eqF (leq_ltn_trans Hk lt_ji)) andbF mul0r.
 Qed.
 
-Fact deriv_tfpsZ (c : K) (f : {tfps K n}) : (c *: f) ^`() = c *: f ^`()%tfps.
+End Composition.
+
+Notation "f \So g" := (comp_tfps g f) : tfps_scope.
+
+
+Section CompComRing.
+
+Variables (R : comRingType) (n : nat).
+Implicit Types (f g h : {tfps R n}) (p : {poly R}).
+
+Fact comp_tfps_is_rmorphism f : multiplicative (comp_tfps f).
 Proof.
-apply/val_inj; apply/polyP => i.
-rewrite coef_poly coef_modXn !coefZ coef_modXn !coefZ coef_poly.
-congr if_expr; rewrite [in RHS]fun_if mulr0 ltnS.
-rewrite [LHS](@fun_if _ _ (fun x => x *+i.+1)) mul0rn.
-move: f; case: n => [p|m p]; last by congr if_expr; rewrite mulrnAr.
-by rewrite [p]tfps_is_cst coef_Tfpsp mul0rn mulr0 if_same.
+split => /= [g1 g2|]; last exact: comp_tfps1.
+case: (boolP (f \in coef0_eq0)) => Hf.
+- rewrite !comp_tfps_coef0_eq0 // mul_tfps_val /=.
+  rewrite -trXn_comp_polyl -?coef_tfpsE ?(eqP Hf) //.
+  rewrite rmorphM /= -trXn_mul /=.
+  by rewrite -[RHS]tfpsK mul_tfps_val /= trXn_trXn.
+- by rewrite !comp_tfps_coef0_neq0 // coef0_tfpsM -rmorphM.
 Qed.
 
-Fact deriv_tfps_is_linear : linear (@deriv_tfps K n).
-Proof. by move => c f g; rewrite deriv_tfpsD deriv_tfpsZ. Qed.
+Canonical comp_tfps_rmorphism f := AddRMorphism (comp_tfps_is_rmorphism f).
+Canonical comp_tfps_lrmorphism f := [lrmorphism of (comp_tfps f)].
 
-Canonical deriv_tfps_additive := Additive deriv_tfps_is_linear. 
-Canonical deriv_tfps_linear := Linear deriv_tfps_is_linear.
+Lemma comp_tfpsA f g h : f \So (g \So h) = (f \So g) \So h.
+Proof.
+case (boolP (h \in coef0_eq0)) => [h0_eq0 | h0_neq0]; first last.
+  rewrite !(comp_tfps_coef0_neq0 _ h0_neq0).
+  by rewrite comp_tfpsCf coef0_comp_tfps.
+case (boolP (g \in coef0_eq0)) => [g0_eq0 | g0_neq0]; first last.
+  by rewrite !(comp_tfps_coef0_neq0 f) ?comp_tfpsC // coef0_eq0_comp.
+rewrite comp_tfps_coef0_eq0 ?coef0_eq0_comp //.
+rewrite !comp_tfps_coef0_eq0 //.
+rewrite -trXn_comp_polyr comp_polyA trXn_comp_polyl //.
+by move: h0_eq0; rewrite coef0_eq0E => /eqP.
+Qed.
 
-(* tests *)
-Example test_deriv_tfps0 : 0 ^`() = 0 :> {tfps K n.-1}.
-Proof. by rewrite linear0. Qed. 
+Lemma coef_comp_poly_cX p c i : (p \Po (c *: 'X))`_i = c ^+ i * p`_i.
+Proof.
+rewrite coef_comp_poly.
+rewrite (eq_bigr (fun j : 'I_ _ =>
+                    c ^+ j * p`_j * (i == j)%:R)) => [|j _]; first last.
+  rewrite -mulr_algl exprMn_comm; last exact: commr_polyX.
+  by rewrite -in_algE -rmorphX mulr_algl coefZ coefXn mulrA [p`_j * _]mulrC.
+case: (ltnP i (size p)) => [lt_isz | le_szi].
+- rewrite (bigD1 (Ordinal lt_isz)) //= big1 ?addr0; first last.
+    move=> [j /= lt_jsz]; rewrite -val_eqE /= eq_sym => /negbTE ->.
+    by rewrite mulr0.
+  by rewrite eqxx mulr1.
+- rewrite nth_default // mulr0 big1 // => [] [j /= lt_jsz] _.
+  by rewrite (gtn_eqF (leq_trans lt_jsz le_szi)) mulr0.
+Qed.
 
-Example test_deriv_tfpsD (f g : {tfps K n}) : 
-    (f + g)^`()%tfps = f^`()%tfps + g^`()%tfps.
-Proof. by rewrite linearD. Qed.
+Lemma coef_comp_tfps_cX f c i : (f \So (c *: \X))`_i = c ^+ i * f`_i.
+Proof.
+case: n f => [|n'] f.
+  rewrite coef_tfps [in RHS]coef_tfps leqn0.
+  case: i => [|i] /=; last by rewrite mulr0.
+  by rewrite -!/(_`_0) expr0 mul1r coef0_comp_tfps.
+case: (leqP i n'.+1) => [lt_in1 | lt_n1i]; first last.
+  rewrite coef_tfps (ltn_geF lt_n1i) nth_default ?mulr0 //.
+  exact: (leq_trans (size_tfps f) lt_n1i).
+rewrite -coef_comp_poly_cX.
+rewrite comp_tfps_coef0_eq0 ?coef0_eq0Z ?tfpsX_in_coef0_eq0 //.
+by rewrite coef_trXn lt_in1 linearZ /= val_tfpsX scale1r.
+Qed.
 
-End Derivative.
+Theorem deriv_tfps_comp f g :
+  f \in coef0_eq0 ->
+  (g \So f)^`() = (g^`()%tfps \So trXnt n.-1 f) * f^`()%tfps.
+Proof.
+rewrite !deriv_tfpsE //.
+move: f g; case: n => [|m] f g f0_eq0.
+  rewrite [f]tfps_is_cst [g]tfps_is_cst.
+  rewrite /trXnt comp_tfpsC.
+  by rewrite !val_tfpsC !derivC trXn0 mulr0.
+rewrite -[RHS]tfpsK [m.+1.-1]/=.
+rewrite /= !comp_tfps_coef0_eq0 ?coef0_eq0_trXnt //.
+rewrite deriv_trXn !trXn_trXn // deriv_comp.
+rewrite -trXn_mul /=; congr (trXn _ (_ * _)).
+by rewrite -trXn_comp_polyr trXn_comp_polyl ?(eqP f0_eq0).
+Qed.
 
-Section MoreDerivative.
+End CompComRing.
 
-Variable (K : fieldType) (m : nat).
 
-Hypothesis char_K_is_zero : [char K] =i pred0.
+Section Lagrange.
+
+Variables R : comUnitRingType.
+Variable n : nat.
+
+
+Section LagrangeFixPoint.
 
-Lemma pw_cst (f : {tfps K m}) : f ^` () = 0 -> {c : K | f = c %:S}.
+Variable g : {tfps R n}.
+Hypothesis gU : g \is a GRing.unit.
+
+
+(** We iterate f := x (g o f) until fixpoint is reached. *)
+(** At each step, the precision is incremented.          *)
+Fixpoint lagriter O : {tfps R O} :=
+  if O is O'.+1 then mulfX ((trXnt O' g) \So (lagriter O')) else 0.
+Definition lagrfix := lagriter n.+1.
+
+Lemma coef0_eq0_lagriter O : lagriter O \in coef0_eq0.
 Proof.
-move: f; case: m => [f _| n f]; first by rewrite [f]tfps_is_cst; exists (f`_0).
-rewrite deriv_tfpsE ; move/eqP ; rewrite -val_eqE /= => /eqP. 
-rewrite modp_small => [derivp_eq0|]; last first.
-+ rewrite size_polyXn.
-  have [->|fN0] := eqVneq f 0; first by rewrite linear0 size_poly0.
-  by rewrite (leq_trans (lt_size_deriv _)) // size_tfps.
-+ move: (p_cst char_K_is_zero derivp_eq0) => [c Hc].
-  by exists c; apply/val_inj => /=; rewrite modCXn.
+by rewrite coef0_eq0E; case: O => [|O]; rewrite ?coef_tfps0 ?coef_mulfX.
 Qed.
+Lemma coef0_eq0_lagrfix : lagrfix \in coef0_eq0.
+Proof. exact: coef0_eq0_lagriter. Qed.
 
-Lemma pw_eq0 (f : {tfps K m}) : 
-    f ^` () = 0 -> {x : K | (val f).[x] = 0} -> f = 0.
+Lemma lagrfixP : lagrfix = mulfX (g \So trXnt n lagrfix).
 Proof.
-rewrite deriv_tfpsE /=; move/eqP ; rewrite -val_eqE /=.
-have [-> _ _ // |fN0] := eqVneq f 0. 
-rewrite modp_small ?size_polyXn ?(leq_trans (lt_size_deriv _)) ?size_tfps //.
-  move/eqP => derivp_eq0; move: (p_cst char_K_is_zero derivp_eq0) => [c Hc].
-  rewrite Hc; move => [x hx]; rewrite hornerC in hx.
-  by apply/val_inj => /=; rewrite Hc hx.
-by rewrite (leq_trans (size_tfps _)) //; clear fN0 f; case: m => [|n].
+rewrite /lagrfix.
+suff rec O : O <= n ->
+     lagriter O.+1 = mulfX (trXnt O g \So trXnt O (lagriter O.+1)).
+  by rewrite [LHS](rec n (leqnn n)) trXnt_id.
+elim: O => [_ | O IHO /ltnW{}/IHO IHO]; apply tfpsP => i.
+  case: i => [_|i]; first by rewrite !coef_mulfX.
+  rewrite ltnS leqn0 => /eqP ->.
+  rewrite !coef_mulfX /= -!/(_`_0).
+  by rewrite comp_tfps0r !coef_tfpsC coef0_comp_tfps.
+case: i => [_|i]; first by rewrite !coef_mulfX.
+rewrite ltnS => le_iO1 /=.
+rewrite -!/(_`_ i.+1) !coef_mulfX /= -/(lagriter O.+1) -!/(_`_ i.+1).
+have lag0 := coef0_eq0_lagriter O.+1.
+move: (lagriter O.+1) => LR in IHO lag0 *.
+have Xlag0 : trXnt O.+1 (mulfX (trXnt O.+1 g \So LR)) \in coef0_eq0.
+  by rewrite coef0_eq0E coef_trXnt coef_mulfX.
+rewrite !coef_comp_tfps //; apply eq_bigr => k _; congr (_ * _).
+rewrite {}[in LHS]IHO -rmorphX coef_trXnt le_iO1.
+set X :=  (_ ^+ k in RHS); have -> : X`_i = (trXnt O.+1 X)`_i.
+  by rewrite {}/X coef_trXnt le_iO1.
+rewrite {}/X rmorphX /= trXnt_mulfX // trXnt_comp; last exact: leqnSn.
+by rewrite trXnt_trXnt.
 Qed.
 
-Lemma pw_eq (f g : {tfps K m}) : 
-               f ^` () = g ^` () -> {x : K | (val f).[x] = (val g).[x]} -> f = g.
+Lemma lagrfix_divP : divfX lagrfix = g \So trXnt n lagrfix.
+Proof. by rewrite {1}lagrfixP mulfXK. Qed.
+Lemma divfX_lagrfix_unit : divfX lagrfix \is a GRing.unit.
 Proof.
-move => H [x Hx].
-apply/eqP ; rewrite -subr_eq0 ; apply/eqP.
-apply: pw_eq0; first by rewrite linearB /= H subrr.
-by exists x ; rewrite -horner_evalE rmorphB /= horner_evalE Hx subrr.
-Qed. 
+by rewrite lagrfix_divP unit_tfpsE coef0_comp_tfps -unit_tfpsE.
+Qed.
 
-Lemma deriv_Tfps0p (f : {tfps K 0}) : f ^` () = 0.
+Lemma lagrfix_inv f :
+  f \in coef0_eq0 -> f = mulfX (g \So trXnt n f) -> (mulfX g^-1) \So f = \X.
 Proof.
-by rewrite [f]tfps_is_cst deriv_tfpsE deriv_modp derivC mod0p rmorph0.
+move=> f0 Heq.
+have tinv0 : trXnt n f \in coef0_eq0 by rewrite coef0_eq0_trXnt.
+rewrite mulfXE rmorphM /= comp_tfpsX //.
+rewrite {1}Heq mulfXM trXnt_comp // trXnt_trXnt // trXnt_id.
+rewrite rmorphV //= divrr ?mulfX1 //.
+by rewrite unit_tfpsE coef0_comp_tfps -unit_tfpsE.
 Qed.
 
-Lemma deriv_tfpsM (f g : {tfps K m}) :
-   (f * g) ^`() = f ^`()%tfps * (Tfpsp m.-1 g) + (Tfpsp m.-1 f) * g ^`()%tfps.
+Lemma lagrfix_invPr : (mulfX g^-1) \So lagrfix = \X.
+Proof. exact: (lagrfix_inv coef0_eq0_lagrfix lagrfixP). Qed.
+
+End LagrangeFixPoint.
+
+Implicit Types (f g : {tfps R n.+1}).
+
+Definition lagrunit f := (f \in coef0_eq0) && (divfX f \is a GRing.unit).
+Definition lagrinv f := lagrfix (divfX f)^-1.
+
+Lemma lagrfixE (f : {tfps R n}) : lagrfix f = lagrinv (mulfX f^-1).
+Proof. by rewrite /lagrinv mulfXK invrK. Qed.
+
+Lemma coef1_comp_tfps f g :
+  f \in coef0_eq0 -> g \in coef0_eq0 -> (f \So g)`_1 = f`_1 * g`_1.
 Proof.
-move : f g; case: m => /= [f g | n f g].
-  rewrite [f]tfps_is_cst [g]tfps_is_cst -tfpsC_mul !deriv_tfpsC mul0r mulr0.
-  by rewrite addr0.
-apply/val_inj; rewrite !deriv_tfpsE //=.   
-rewrite deriv_modp derivM modp_mul modp_mul2 -modp_add modp_mod !modp_add.
-by rewrite !modp_mul; congr (_ + _); rewrite mulrC [in RHS]mulrC modp_mul.
+move=> f0 g0.
+rewrite coef_comp_tfps // big_ord_recl (eqP f0) mul0r add0r.
+by rewrite big_ord_recl /= big_ord0 /bump /= -!/(_`_ 1) !add1n addr0.
 Qed.
 
-Fact TfpsVf n p (f : {tfps K p}) :
-  n <= p ->
-  Tfpsp n (f^-1) = (Tfpsp n f) ^-1.
+Lemma divfX_unitE f : (divfX f \is a GRing.unit) = (f`_1 \is a GRing.unit).
+Proof. by rewrite unit_tfpsE coef_divfX. Qed.
+
+Lemma lagrunit_comp : {in lagrunit &, forall f g, lagrunit (f \So g) }.
 Proof.
-move=> leq_mn.
-have [/eqP p0_eq0|p0_neq0] := eqVneq f`_0 0.
-  by rewrite ?(invr_out, unit_tfpsE, nth0_Tfpsp, negbK).
-apply: (@mulrI _ (Tfpsp _ f)); rewrite ?divrr ?(unit_tfpsE, nth0_Tfpsp) //.
-rewrite -rmorphM; apply/val_inj => /=.
-rewrite -(@modp_modp K _ 'X^n.+1 'X^p.+1); last by rewrite dvdp_exp2l.
-by rewrite -val_mul_tfps divrr ?unit_tfpsE // modCXn.
-Qed.
-
-Lemma deriv_tfpsV (f : {tfps K m}) :
-  f \notin (@coef0_is_0 _ _) ->
-  (f ^-1) ^`() = - f ^`()%tfps / Tfpsp m.-1 (f ^+ 2).
-Proof.
-move => p0_neq0.
-move/eqP: (eq_refl (f / f)).
-rewrite {2}divrr; last by rewrite unit_tfpsE.
-move/(congr1 (@deriv_tfps K m)).
-rewrite deriv_tfpsM onefE deriv_tfpsC.
-move/eqP ; rewrite addrC addr_eq0 mulrC.
-move/eqP/(congr1 (fun x => x / (Tfpsp m.-1 f))).
-rewrite -mulrA divrr; last by rewrite unit_tfpsE nth0_Tfpsp.
-rewrite mulr1 => ->.
-rewrite !mulNr; congr (- _).
-rewrite -mulrA; congr (_ * _).
-rewrite TfpsVf // ?leq_pred // -invrM ?unit_tfpsE ?nth0_Tfpsp //; congr (_ ^-1).
-rewrite -rmorphM /=; apply/val_inj => /=.
-by rewrite modp_modp // dvdp_exp2l // (leq_ltn_trans (leq_pred _)).
-Qed.
-                                                             
-Lemma deriv_div_tfps (f g : {tfps K m}) :
-  g`_0 != 0 ->
-  (f / g) ^`() = (f^`()%tfps * Tfpsp m.-1 g - Tfpsp m.-1 f * g ^`()%tfps)
-                                                    / (Tfpsp m.-1 (g ^+ 2)).
-Proof.
-move => g0_neq0.
-rewrite deriv_tfpsM deriv_tfpsV // mulrBl mulrA mulrN mulNr.
-congr (_ - _); rewrite -mulrA; congr (_ * _).
-rewrite TfpsVf //; last exact: leq_pred.
-rewrite expr2 ?leq_pred //. 
-have -> : Tfpsp m.-1 (g * g) = Tfpsp m.-1 ((val g) * g).
-  apply/val_inj => /=.
-  rewrite modp_modp ?dvdp_exp2l //. 
-  by clear g0_neq0 f g; case: m => //=. 
-rewrite rmorphM /= invrM ?Tfpsp_is_unit ?nth_Tfpsp //.
-by rewrite mulrA divrr ?Tfpsp_is_unit ?nth_Tfpsp // mul1r.
-Qed. 
-
-End MoreDerivative. 
+rewrite /lagrunit => f g /andP [f0 f1] /andP [g0 g1].
+rewrite coef0_eq0_comp f0 /=.
+rewrite unit_tfpsE coef_divfX /= -/(_`_1).
+by rewrite coef1_comp_tfps // unitrM -!divfX_unitE f1 g1.
+Qed.
 
-Section Primitive.
+Lemma lagrunitV : {in lagrunit, forall f, lagrunit (lagrinv f) }.
+Proof.
+rewrite /lagrunit => f /andP [H0 H1].
+by rewrite coef0_eq0_lagrfix divfX_lagrfix_unit // unitrV.
+Qed.
 
-Variables (K : fieldType) (n : nat).
+Lemma lagrinvPr : {in lagrunit, forall f, f \So (lagrinv f) = \X }.
+Proof.
+rewrite /lagrinv/lagrunit => f /andP [H0 H1].
+have /lagrfix_invPr : (divfX f)^-1 \is a GRing.unit by rewrite unitrV.
+by rewrite invrK divfXK.
+Qed.
 
-Definition prim (p : {poly K}) :=
-    \poly_(i < (size p).+1) (p`_i.-1 *+ (i != 0%N) / (i%:R)).
+Lemma lagrinvPl : {in lagrunit, forall f, (lagrinv f) \So f = \X }.
+Proof.
+move=> f Hf.
+(** Standard group theoretic argument: right inverse is inverse *)
+have idemp_neutral g : lagrunit g -> g \So g = g -> g = \X.
+  move=> Hinv Hid; rewrite -(comp_tfpsXr g) // -(lagrinvPr Hinv).
+  by rewrite comp_tfpsA {}Hid.
+apply idemp_neutral; first exact: lagrunit_comp (lagrunitV Hf) Hf.
+rewrite comp_tfpsA -[X in (X \So f) = _]comp_tfpsA lagrinvPr //.
+by rewrite comp_tfpsXr.
+Qed.
 
-Definition prim_tfps (n : nat) : {tfps K n} -> {tfps K n.+1} :=
-    fun f => [tfps s => f`_s.-1 *+ (s != 0%N) / s%:R].
+Lemma lagrinvPr_uniq f g :
+  f \in lagrunit -> f \So g = \X -> g = lagrinv f.
+Proof.
+move=> f_lag Heq.
+have g0 : g \in coef0_eq0.
+  rewrite -[_ \in _]negbK; apply/negP => H.
+  move: Heq; rewrite comp_tfps_coef0_neq0 //.
+  move => /(congr1 (fun s : {tfps _ _} => s`_1)).
+  rewrite coef_tfpsX coef_tfpsC /= => /esym/eqP.
+  by rewrite mulr1 oner_eq0.
+(** Standard group theoretic argument: right inverse is uniq *)
+move: Heq => /(congr1 (fun s => lagrinv f \So s)).
+by rewrite comp_tfpsA lagrinvPl // comp_tfpsX // comp_tfpsXr.
+Qed.
 
-Local Notation "\int p" := (prim p) (at level 2).
+Lemma lagrinvPl_uniq f g :
+  f \in lagrunit -> g \So f = \X -> g = lagrinv f.
+Proof.
+move=> f_lag /(congr1 (fun s => s \So lagrinv f)).
+(** Standard group theoretic argument: left inverse is uniq *)
+rewrite -comp_tfpsA lagrinvPr // comp_tfpsXr // comp_tfpsX //.
+exact: coef0_eq0_lagrfix.
+Qed.
 
-Lemma coef_prim (p : {poly K}) (i : nat) :
-                        (\int p)`_i = if i == 0%N then 0 else p`_i.-1 / (i%:R).
+Lemma lagrinvK : {in lagrunit, involutive lagrinv}.
 Proof.
-case: i => [| i]; first by rewrite eqxx coef_poly invr0 mulr0.
-rewrite succnK eqn0Ngt ltn0Sn coef_poly.
-rewrite eqn0Ngt ltn0Sn /= -{3}[p]coefK coef_poly ltnS.
-by case: (i < size p) => //; rewrite mul0r.
+(** Standard group theoretic argument: inverse is involutive *)
+move=> f Hf.
+by apply/esym/lagrinvPl_uniq; [apply: lagrunitV | apply: lagrinvPr].
+Qed.
+
+Lemma lagrfix_invPl :
+  {in GRing.unit, forall g : {tfps R n}, lagrfix g \So mulfX g^-1 = \X}.
+Proof.
+move=> g gU.
+rewrite lagrfixE; apply: lagrinvPl.
+rewrite /lagrunit unfold_in coef0_eq0E coef_mulfX /= eqxx /=.
+by rewrite divfX_unitE coef_mulfX /= -/(_`_0) -unit_tfpsE unitrV.
+Qed.
+
+Lemma lagrfix_uniq (g : {tfps R n}) : g \in GRing.unit ->
+  forall f, f = mulfX (g \So trXnt n f) -> f = lagrfix g.
+Proof.
+move=> gU f Hf.
+rewrite lagrfixE; apply lagrinvPr_uniq.
+- by rewrite /lagrunit unfold_in coef0_eq0E coef_mulfX mulfXK unitrV /= eqxx.
+- by apply: lagrfix_inv => //; rewrite Hf coef0_eq0E coef_mulfX.
+Qed.
+
+End Lagrange.
+
+
+Section LagrangeTheorem.
+
+Variables R : comUnitRingType.
+Hypothesis nat_unit : forall i, i.+1%:R \is a @GRing.unit R.
+
+(* TODO: nat_unit is not needed here *)
+Lemma mulfX_deriv_expE n (g : {tfps R n.+1}) i :
+  (g ^+ i.+1 - mulfX g^`()%tfps * g ^+ i)`_i.+1 = 0.
+Proof.
+rewrite mulfXM mulrC rmorphX /= -/(_`_i.+1).
+apply (mulrI (nat_unit i)); rewrite mulr0 -!coeftZ scalerBr.
+rewrite -linearZ /= !scaler_nat -(derivX_tfps g i.+1) -/(_`_i.+1).
+by rewrite coeftB coef_mulfX coef_deriv_tfps /= -!/(_`_i.+1) coeftMn subrr.
+Qed.
+
+Theorem Lagrange_Bürmann_exp n (g : {tfps R n}) i k :
+  g \in GRing.unit ->
+  k <= i <= n.+1 -> ((lagrfix g) ^+ k)`_i *+ i = (g ^+ i)`_(i - k) *+ k.
+Proof.
+(* We first deal with trivial cases                                    *)
+case: n g => [|n] g gU.
+  rewrite /lagrfix /= (tfps_is_cst g) comp_tfps0r.
+  move: gU; rewrite unit_tfpsE; move: (g`_0) => g0 {g} gU.
+  rewrite trXntC coef_tfpsC /=.
+  case: k => [|[|k]].
+  - rewrite mulr0n expr0 coef1.
+    by case: i => [|i]/= _; rewrite ?mulr0n ?mul0rn.
+  - move=> /andP [le1i lei1].
+    have {le1i lei1} -> : i = 1%N by apply anti_leq; rewrite le1i lei1.
+    by rewrite !expr1 !mulr1n subSS coef_mulfX /=.
+  - move=> /andP [leki lei1].
+    by have:= leq_trans leki lei1; rewrite ltnS ltn0.
+case: k i => [|k] [|i]; rewrite ?(expr0, subn0, coef1, mulr0n, mul0rn) //.
+rewrite subSS !ltnS => /andP [le_ki le_in].
+have Xg0 : mulfX g^-1 \in coef0_eq0 by rewrite coef0_eq0E coef_mulfX.
+(* The RHS is ((\X ^+ k.+1)^`() * g ^+ i.+1)`_i                        *)
+have:= congr1 (fun s => (s ^+ k.+1)^`()) (lagrfix_invPl gU).
+rewrite -rmorphX /= {1}(tfps_def (lagrfix g ^+ k.+1)) rmorph_sum /=.
+move: (lagrfix g ^+ k.+1) => LGRF.
+rewrite raddf_sum /= derivX_tfps deriv_tfpsX mulr1 /= trXnt_tfpsX.
+move=> /(congr1 (fun s => (s * g ^+ i.+1)`_i)).
+rewrite mulrnAl -mulrnAr.
+rewrite coef_tfpsXnM (leq_gtF le_ki) le_in coeftMn => <- {k le_ki}.
+rewrite mulr_suml coeft_sum -/(_`_i.+1).
+(* We extract the i.+1 term of the sum                                 *)
+have Hi : i.+1 < n.+3 by rewrite ltnS (leq_ltn_trans le_in).
+rewrite (bigD1 (Ordinal Hi)) //= -/(_`_i.+1).
+move: (LGRF`_i.+1) => Co.
+rewrite !linearZ /= -scalerAl coeftZ rmorphX /= comp_tfpsX //.
+rewrite derivX_tfps /= !mulrnAl coeftMn /= mulrnAr -mulrnAl.
+rewrite -mulrA coefM_tfps le_in big_ord_recr /=.
+rewrite subnn coef0_tfpsM coef_deriv_tfps coef_mulfX /= -!/(_`_0) mulr1n.
+rewrite {2}exprS coef0_tfpsM [g^-1`_0 * _]mulrA coef0_tfpsV //.
+rewrite mulVr -?unit_tfpsE // mul1r.
+rewrite -rmorphX /= coef_trXnt le_in -!/(_`_0).
+rewrite coef_mulfX_exp ?(leq_trans le_in) //.
+rewrite -coef0_tfpsM exprVn mulVr ?rpredX // coef1 /=.
+(* All the other terms vanishe.                                        *)
+rewrite !big1 ?add0r ?addr0 ?mulr1 //; first last.
+  move=> [j /= lt_ji] _.
+  rewrite coef_trXnt (leq_trans (ltnW lt_ji) le_in).
+  by rewrite coef_mulfX_exp_lt // mul0r.
+move=> [j Hj]; rewrite -val_eqE /= {Hi} => Hneq.
+rewrite !linearZ /= -scalerAl coeftZ rmorphX /= comp_tfpsX //.
+rewrite [X in _ * X](_ : _ = 0) ?mulr0 // {LGRF}.
+(* We don't have the notion of residue. As a consequence the following *)
+(* is a little bit convoluted...                                       *)
+(* First, lets get rid of the first mulfX...                           *)
+rewrite derivX_tfps /= mulrnAl coeftMn.
+case: j Hneq Hj => // j /=; rewrite eqSS !ltnS => Hij le_jn1.
+rewrite [X in X *+ _](_ : _ = 0) ?mul0rn //.
+rewrite mulfXE derivM_tfps deriv_tfpsX mul1r /= deriv_trXnt.
+rewrite trXnt_tfpsX trXnt_trXnt ?ltnS // trXnt_id.
+rewrite -[X in _ + X]mulfXE.
+rewrite -rmorphX /= exprMn_comm; last exact: (commr_sym (commr_tfpsX _)).
+rewrite !rmorphM !rmorphX /= trXnt_tfpsX trXnt_trXnt // trXnt_id.
+rewrite -!mulrA coef_tfpsXnM le_in; case ltnP => //= le_ji.
+(* We rearange to have everything expressed in [i - j]                 *)
+have {Hij le_ji} lt_ji : j < i by rewrite ltn_neqAle Hij le_ji.
+rewrite mulrC -mulrA exprVn -exprB ?(leq_trans (ltnW lt_ji)) //.
+rewrite (subSn (ltnW _)) // exprS mulrA mulrDl mulVr //.
+move: lt_ji; rewrite -subn_gt0.
+case: (i - j)%N (leq_subr j i) => // d lt_di _ {j le_jn1}.
+(* We gather all the [g] and conclude                                  *)
+rewrite mulfXM derivV_tfps //= -/(_`_d.+1).
+rewrite !mulNr raddfN /= -/(_`_d.+1) -trXntV // -mulrA -trXntM // -!mulfXM.
+rewrite mulrDl mul1r mulNr -mulrA.
+rewrite {2}exprS !mulrA -[_ * g]mulrA -expr2 divrK ?unitrX //.
+exact: mulfX_deriv_expE.
+Qed.
+
+Theorem coef_lagrfix n (g : {tfps R n}) i :
+  g \in GRing.unit -> (lagrfix g)`_i.+1 = (g ^+ i.+1)`_i / i.+1%:R.
+Proof.
+move/Lagrange_Bürmann_exp => HL.
+case: (ltnP i n.+1) => [lt_in1 | le_ni]; first last.
+  by rewrite coef_tfps (leq_gtF le_ni) coef_tfps (ltn_geF le_ni) mul0r.
+have /HL : 1 <= i.+1 <= n.+1 by rewrite lt_in1.
+rewrite subSS subn0 mulr1n expr1 => <-.
+by rewrite -mulr_natr mulrK.
+Qed.
+
+
+Theorem Lagrange_Bürmann n (g : {tfps R n}) (h : {tfps R n.+1}) i  :
+  g \in GRing.unit ->
+  (h \So lagrfix g)`_i.+1 = (h^`()%tfps * g ^+ i.+1)`_i / i.+1%:R.
+Proof.
+move=> gU.
+have lg0 := coef0_eq0_lagrfix g.
+(* We argue by linearity from the previous statement *)
+rewrite (tfps_def h) !(raddf_sum, mulr_suml, coeft_sum).
+apply eq_bigr => [[k /=]]; rewrite ltnS => le_kn2 _.
+rewrite !linearZ /= -/(_`_i.+1) -scalerAl !coeftZ -mulrA; congr (_ * _).
+case: k le_kn2 => [_|k lt_kn2].
+  (* When k = 0 the result is trivial *)
+  by rewrite expr0 comp_tfps1 coef1 deriv_tfps1 mul0r coef0 mul0r.
+rewrite rmorphX /= comp_tfpsX // -/(_`_i.+1).
+rewrite [LHS]coef_tfps [in RHS]coef_tfps ltnS.
+case: leqP => [le_in1|_]; last by rewrite mul0r.
+case: (ltnP i k) => [lt_ik | le_ki].
+  (* If i < k both side vanishes *)
+  rewrite coefX_tfps_eq0 ?ltnS //.
+  rewrite [X in X / _](_ : _ = 0) ?mul0r //.
+  rewrite coefM_tfps le_in1; apply big1 => [[j /=]]; rewrite ltnS => le_ji _.
+  rewrite coef_deriv_tfps.
+  rewrite coef_tfpsXn eqSS (ltn_eqF (leq_ltn_trans le_ji lt_ik)).
+  by rewrite andbF mul0rn mul0r.
+(* Else we conclude by the previous theorem *)
+apply (mulIr (nat_unit i)); rewrite divrK // mulr_natr.
+rewrite Lagrange_Bürmann_exp //; last by rewrite !ltnS le_ki le_in1.
+rewrite subSS derivX_tfps /= trXnt_tfpsX deriv_tfpsX mulr1.
+rewrite mulrnAl -mulrnAr coef_tfpsXnM le_in1 (leq_gtF le_ki).
+by rewrite coeftMn.
+Qed.
+
+
+(** This form of statement doesn't allow to compute the n.+2 coefficient *)
+Theorem Lagrange_Bürmann_exp2 n (g : {tfps R n.+1}) i k :
+  g \in GRing.unit ->
+  k <= i <= n.+1 -> ((lagrfix g) ^+ k)`_i =
+                    ((1 - mulfX g^`()%tfps / g) * \X ^+ k * g ^+ i)`_i.
+Proof.
+move=> gU.
+case: k i => [|k] [|i] Hki //.
+- by rewrite !expr0 !mulr1 coeftB coef0_tfpsM coef_mulfX mul0r subr0.
+- rewrite !expr0 !mulr1 coef_tfps1 exprS mulrA !mulrBl mul1r.
+  by rewrite divrK //= -!/(_`_i.+1) -exprS mulfX_deriv_expE.
+move: Hki; rewrite !ltnS => /andP [le_ki le_in].
+have le_in1 := (leq_trans le_in (leqnSn _)).
+rewrite -mulrA [\X^+_ * _]mulrC mulrA mulrC !mulrBl mul1r.
+rewrite (exprS g i) mulrA divrK // -exprS.
+rewrite (exprS \X k) -mulrA coef_tfpsXM /= ltnS le_in -/(_`_i.+1).
+apply (mulIr (nat_unit i)).
+rewrite mulr_natr Lagrange_Bürmann_exp // ?ltnS ?le_ki ?le_in1 //.
+have := erefl (\X ^+ k * mulfX (g ^+ i.+1))^`().
+rewrite {2}mulfXE mulrA [_ * \X]mulrC -exprS.
+rewrite [X in _ = X]derivM_tfps derivX_tfps /=.
+rewrite trXnt_trXnt // trXnt_id trXnt_tfpsX deriv_tfpsX mulr1 mulrnAl.
+move/(congr1 (fun s : {tfps R _} => s`_i)).
+rewrite coeftD coeftMn [(\X^+k * _)`_i]coef_tfpsXnM le_in1 (leq_gtF le_ki).
+set X := (X in _ = _ + X); move=> /(congr1 (fun s => s - X)).
+rewrite addrK => <-.
+rewrite {}/X deriv_trXnt [\Xo(n.+2) ^+ k.+1]exprS rmorphM /= trXnt_tfpsX.
+rewrite [\X * _]mulrC -!mulrA -mulfXE rmorphX /= trXnt_tfpsX -/(_`_i.+1).
+rewrite coef_deriv_tfps.
+rewrite !coef_tfpsXnM le_in1 ltnS le_in1 (leq_gtF (leq_trans le_ki (leqnSn _))).
+rewrite (leq_gtF le_ki) coef_mulfX -/(leq _ _) (leq_gtF le_ki).
+rewrite subSn //= coeftB mulrBl mulr_natr; congr (_ - _).
+rewrite mulfXM !coef_mulfX -/(leq _ _).
+case: leqP; rewrite ?mul0r // => lt_ki.
+by rewrite derivX_tfps /= coeftMn mulrC rmorphX /= mulr_natr.
+Qed.
+
+Theorem Lagrange_Bürmann2 n (g h : {tfps R n.+1}) i :
+  g \in GRing.unit ->
+  (h \So (trXnt n.+1 (lagrfix g)))`_i =
+  ((1 - mulfX g^`()%tfps / g) * h * g ^+ i)`_i.
+Proof.
+move=> uG.
+case: (leqP i n.+1) => [le_in1 | lt_n1i]; first last.
+  by rewrite coef_tfps (ltn_geF lt_n1i) coef_tfps (ltn_geF lt_n1i).
+rewrite (tfps_def h) !(raddf_sum, mulr_suml, mulr_sumr, coeft_sum) /=.
+apply eq_bigr => [[k /=]]; rewrite ltnS => le_kn2 _.
+rewrite !linearZ /= -mulrA mulrC -!scalerAl !coeftZ; congr (_ * _).
+rewrite rmorphX /= comp_tfpsX ?coef0_eq0_trXnt ?coef0_eq0_lagrfix //.
+rewrite -rmorphX coef_trXnt le_in1.
+case: (leqP k i) => [le_ki | lt_ik]; first last.
+  rewrite coefX_tfps_eq0 ?coef0_eq0_lagrfix //.
+  by rewrite -mulrA coef_tfpsXnM lt_ik.
+rewrite Lagrange_Bürmann_exp2 ?le_in1 ?andbT //.
+by rewrite [in RHS]mulrC mulrA.
+Qed.
+
+End LagrangeTheorem.
+
+
+Section ExpLog.
+
+Variables (R : unitRingType) (n : nat).
+Implicit Types (f g : {tfps R n}).
+
+Definition exp f : {tfps R n} :=
+  if f \notin coef0_eq0 then 0 else
+  \sum_(i < n.+1) i`!%:R ^-1 *: f ^+ i.
+
+Definition log f : {tfps R n} :=
+  if f \notin coef0_eq1 then 0 else
+  - \sum_(1 <= i < n.+1) i%:R ^-1 *: (1 - f) ^+ i.
+
+Definition expr_tfps (c : R) f := exp (c *: log f).
+
+Lemma exp_coef0_eq0 f : f \in coef0_eq0 ->
+  exp f = \sum_(i < n.+1) i`!%:R ^-1 *: f ^+ i.
+Proof. by rewrite /exp => ->. Qed.
+
+Lemma exp_coef0_eq0_val f : f \in coef0_eq0 ->
+  exp f = trXn n (\sum_(i < n.+1) i`!%:R ^-1 *: (tfps f) ^+ i).
+Proof.
+rewrite /exp => ->; rewrite /= !raddf_sum; apply eq_bigr => i _ /=.
+by rewrite -[LHS]tfpsK !linearZ /= exp_tfps_val trXn_trXn.
 Qed.
 
-Lemma coef0_prim (p : {poly K}) : (\int p)`_0 = 0.
-Proof. by rewrite coef_prim eqxx. Qed.
+Lemma exp_coef0_isnt_0 f : f \notin coef0_eq0 -> exp f = 0.
+Proof. by rewrite /exp => /negPf ->. Qed.
 
-Lemma primC (c : K) : \int (c%:P) = c *: 'X.
+Lemma exp0 : exp (0 : {tfps R n}) = 1.
 Proof.
-apply/polyP => i.
-rewrite /prim /prim coef_poly size_polyC -[c *: 'X]coefK.
-have [-> | c_neq0 ] := eqVneq c 0.
-  rewrite eqxx /= scale0r size_poly0 coef_poly ltn0; case: i => [|i].
-    by rewrite invr0 mulr0.
-    by rewrite coefC.
-rewrite c_neq0 /= coef_poly size_scale // size_polyX coefZ coefX.
-congr if_expr; case: i => [|i]; first by rewrite invr0 !mulr0.
-rewrite coefC mulr1n.
-case: i => [|i]; first by rewrite !eqxx invr1.
-by rewrite /= mul0r mulr0.
+apply/tfpsP => i le_in.
+rewrite exp_coef0_eq0 ?rpred0 // !coeft_sum /=.
+rewrite big_ord_recl /= fact0 invr1 expr0 alg_tfpsC tfpsC1.
+rewrite big1 ?addr0 // => [] [j ] _ _ /=.
+by rewrite /bump /= add1n expr0n /= scaler0 coef0.
 Qed.
 
-Lemma primX : \int 'X = (2%:R) ^-1 *: 'X ^+2.
+Lemma expC (c : R) : exp (c%:S) = (c == 0)%:R%:S :> {tfps R n}.
 Proof.
-rewrite /prim /prim size_polyX ; apply/polyP => i.
-rewrite coef_poly coefZ coefXn coefX.
-case: i => [|i]; first by rewrite invr0 !mulr0.
-rewrite eqn0Ngt ltn0Sn /=; case: i => [ | i ] ; first by rewrite mul0r mulr0.
-case: i => [|i]; first by rewrite mul1r mulr1.
-by rewrite mulr0.
+case (boolP (c%:S \in @coef0_eq0 R n)) => [| p0N0].
+- rewrite coef0_eq0E coef_tfpsC /= => /eqP ->.
+  by rewrite eq_refl tfpsC0 tfpsC1 exp0.
+- rewrite exp_coef0_isnt_0 //.
+  move: p0N0; rewrite coef0_eq0E coef_tfpsC /= => /negbTE ->.
+  by rewrite rmorph0.
 Qed.
 
-Lemma prim_tfpsXn (m : nat): \int ('X ^+ m) = (m.+1 %:R) ^-1 *: 'X ^+ m.+1.
+Lemma log_coef0_eq1 f : f \in coef0_eq1 ->
+  log f = - \sum_(1 <= i < n.+1) i%:R ^-1 *: (1 - f) ^+i.
+Proof. by rewrite /log => ->. Qed.
+
+Lemma log_coef0_eq1_val f : f \in coef0_eq1 ->
+  log f = trXn n (- \sum_(1 <= i < n.+1) i%:R ^-1 *: (1 - val f) ^+i).
 Proof.
-rewrite /prim /prim size_polyXn ; apply/polyP => i.
-rewrite coefZ !coefXn coef_poly !coefXn.
-have [-> | /negbTE i_neq_Sm ] := eqVneq i m.+1.
-  by rewrite eqxx ltnSn mulr1 eqxx mul1r.
-rewrite i_neq_Sm /= mulr0 ; case: (i < m.+2) => [] //.
-have [ -> | /negbTE i_neq0 ] := eqVneq i 0%N; first by rewrite eqxx invr0 mulr0.
-rewrite i_neq0 ; move/negbT : i_neq0 ; move/negbT : i_neq_Sm.
-case: i => [ // | i ].
-by rewrite (inj_eq succn_inj) => /negbTE -> _ ; rewrite mul0r.
+rewrite /log => ->; rewrite /= !raddf_sum; apply eq_bigr => i _ /=.
+by rewrite -[LHS]tfpsK !linearZ !linearN /= exp_tfps_val trXn_trXn.
 Qed.
 
-Fact prim_is_linear : linear prim.
+Lemma log_coef0_isnt_1 f : f \notin coef0_eq1 -> log f = 0.
+Proof. by rewrite /log => /negPf ->. Qed.
+
+Lemma log1 : log (1 : {tfps R n}) = 0.
 Proof.
-move => k p q ; apply/polyP => i.
-case: i => [ | i]; first by rewrite coefD coefZ !coef0_prim mulr0 addr0.
-by rewrite !(coef_prim, coefD, coefZ) mulrDl -mulrA.
-Qed. 
+apply/tfpsP => j Hj; rewrite log_coef0_eq1 ?rpred1 // coef0 subrr.
+rewrite coefN big_nat big1 ?coef0 ?oppr0 // => i /andP [Hi _].
+by rewrite expr0n -[i == 0%N]negbK -lt0n Hi /= scaler0.
+Qed.
 
-Canonical prim_additive := Additive prim_is_linear.
-Canonical prim_linear := Linear prim_is_linear.
+Lemma exp_in_coef0_eq1 f : (exp f \in coef0_eq1) = (f \in coef0_eq0).
+Proof.
+apply/idP/idP => [| Hf].
+- apply/contraLR => /exp_coef0_isnt_0 ->.
+  by rewrite coef0_eq1E coef0 eq_sym oner_eq0.
+- rewrite exp_coef0_eq0 //.
+  rewrite big_ord_recl /= fact0 invr1 scale1r expr0.
+  rewrite addrC coef0_eq1_add01 ?rpred1 //.
+  apply rpred_sum => [i _].
+  by rewrite coef0_eq0Z // coef0_eq0X.
+Qed.
 
-(* tests *)
-Fact prim0 : prim 0 = 0.
-Proof. exact: linear0. Qed.
+Lemma coef0_exp f : f \in coef0_eq0 -> (exp f)`_0 = 1.
+Proof. by rewrite -exp_in_coef0_eq1 coef0_eq1E => /eqP. Qed.
 
-Fact primD : {morph prim : p q / p + q}.
-Proof. exact: linearD. Qed.
+Lemma exp_unit f : f \in coef0_eq0 -> exp f \is a GRing.unit.
+Proof. by rewrite -exp_in_coef0_eq1; apply coef0_eq1_unit. Qed.
 
-Fact primN : {morph prim : p / - p}.
-Proof. exact: linearN. Qed.
+Lemma log_in_coef0_eq0 f : log f \in coef0_eq0.
+Proof.
+case (boolP (f \in coef0_eq1)) => [f0_eq1|f0_neq1]; last first.
+  by rewrite log_coef0_isnt_1 // rpred0.
+rewrite log_coef0_eq1 //.
+rewrite rpredN big_nat rpred_sum // => [[|i]] // _.
+by rewrite coef0_eq0Z // coef0_eq0X // -coef0_eq10.
+Qed.
 
-Fact primB : {morph prim : p q / p - q}.
-Proof. exact: linearB. Qed.
+Lemma coef0_log f : (log f)`_0 = 0.
+Proof. by have := log_in_coef0_eq0 f; rewrite coef0_eq0E => /eqP. Qed.
 
-Hypothesis char_K_is_zero : [char K] =i pred0.
+End ExpLog.
+
+Arguments log {R n}.
+Arguments exp {R n}.
+
+Notation "f ^^ r" := (expr_tfps r f) : tfps_scope.
 
-Fact natmul_inj (m : nat) : (m%:R == 0 :> K) = (m == 0%N).
-Proof. by move/(charf0P K)/(_ m) : char_K_is_zero. Qed.
 
-Lemma pred_size_prim (p : {poly K}) : (size (prim p)).-1 = size p.
+
+Module TFPSUnitRing.
+
+Section PrimitiveUnitRing.
+
+Variable R : unitRingType.
+Hypothesis nat_unit : forall i, i.+1%:R \is a @GRing.unit R.
+Variable n : nat.
+
+Fact natmul_inj (m : nat) : (m%:R == 0 :> R) = (m == 0%N).
 Proof.
-have [->|/negbTE p_neq0] := eqVneq p 0; first by rewrite prim0 size_poly0.
-rewrite size_poly_eq // size_poly_eq0 p_neq0 -lead_coefE mulf_neq0 //.
-  by rewrite lead_coef_eq0 p_neq0.
-by rewrite invr_eq0 natmul_inj // size_poly_eq0 p_neq0.
+case: m => [|m]; first by rewrite eq_refl; apply/eqP.
+rewrite {2}/eq_op /=.
+apply/negP => /eqP/(congr1 (fun x => x \is a GRing.unit)).
+by rewrite nat_unit unitr0.
 Qed.
 
-Lemma primK : cancel prim (@deriv K).
+Lemma pred_size_prim (p : {poly R}) : (size (prim p)).-1 = size p.
 Proof.
-move => p.
+have [->|p_neq0] := eqVneq p 0; first by rewrite prim0 size_poly0.
+rewrite size_poly_eq // size_poly_eq0 p_neq0 -lead_coefE /=.
+have:= p_neq0; rewrite -size_poly_eq0.
+case: (size p) => // sz _.
+apply/negP => /eqP/(congr1 (fun x => x * sz.+1%:R))/eqP.
+by rewrite mul0r divrK // mulr1n lead_coef_eq0 (negbTE p_neq0).
+Qed.
+
+Lemma primK : cancel (@prim R) (@deriv R).
+Proof.
+move=> p.
 rewrite /prim -{3}[p]coefK ; apply/polyP => i.
 rewrite coef_deriv !coef_poly ltnS.
 case: (_ < _); last by rewrite mul0rn.
-by rewrite eqn0Ngt ltn0Sn -mulr_natr mulrAC -mulrA divff ?natmul_inj // mulr1.
+by rewrite eqn0Ngt ltn0Sn -mulr_natr /= divrK.
+Qed.
+
+Implicit Types (f g : {tfps R n}).
+
+Lemma prim_tfpsK : cancel (@prim_tfps R n) (@deriv_tfps R n.+1).
+Proof.
+move=> p; apply/tfpsP => i le_in.
+rewrite coef_deriv_tfps coef_prim_tfps.
+by rewrite -coef_deriv primK -coef_tfpsE.
 Qed.
 
-Fact prim_tfps_is_linear : linear (@prim_tfps n).
+Lemma deriv_tfpsK :
+  {in @coef0_eq0 R n.+1, cancel (@deriv_tfps R _) (@prim_tfps R _)}.
 Proof.
-move => k p q; apply/val_inj => /=.
-apply/polyP => i.
-rewrite coefD coef_modXn coefZ !coef_poly.
-case: (i < _) => /=; last by rewrite addr0.
-rewrite coefD mulrnDl mulrDl; congr (_ + _); rewrite coef_modXn coefZ.
-case: i => [|i /=]; first by rewrite eqxx mulr0n invr0 !mulr0.
-have [_|/leq_sizeP big_i] := ltnP; first by rewrite mulrA.
-rewrite mul0rn mul0r big_i; first by rewrite mul0rn mul0r mulr0.
-by rewrite size_tfps.  
+move=> f; rewrite coef0_eq0E => /eqP f0_eq0.
+apply/tfpsP => i _.
+rewrite coef_prim_tfps coef_prim coef_deriv_tfps.
+case: i => [|i]; first by rewrite eq_refl f0_eq0.
+by rewrite [_.+1.-1]/= -mulr_natr mulrK.
 Qed.
 
-Canonical prim_tfps_linear := Linear prim_tfps_is_linear.
+End PrimitiveUnitRing.
 
-(* tests *)
-Fact prim_tfps0 : @prim_tfps n 0 = 0.
-Proof. exact: linear0. Qed.
 
-Fact prim_tfpsD : {morph (@prim_tfps n) : p q / p + q}.
-Proof. exact: linearD. Qed.
+Section ExpMorph.
 
-Lemma prim_tfpsK : cancel (@prim_tfps n) (@deriv_tfps K n.+1).
+Variable R : comUnitRingType.
+Hypothesis nat_unit : forall i, i.+1%:R \is a @GRing.unit R.
+Variable n : nat.
+
+
+Lemma nat_unit_alg (A : unitAlgType R) i : i.+1%:R \is a @GRing.unit A.
+Proof. by rewrite -scaler_nat scaler_unit ?unitr1 ?nat_unit. Qed.
+
+
+Implicit Types (f g : {tfps R n}).
+
+Lemma fact_unit m : m`!%:R \is a @GRing.unit R.
+Proof. by have:= fact_gt0 m; rewrite lt0n; case: m`!. Qed.
+
+Theorem expD : {in (@coef0_eq0 R n) &, {morph exp : f g / f + g >-> f * g}}.
 Proof.
-move=> p; apply/val_inj; apply/polyP => i; rewrite coef_poly.
-have [small_i|/leq_sizeP big_i] := ltnP; last by rewrite big_i // size_tfps.
-rewrite coef_poly /= ltnS small_i mulr1n -mulr_natr -mulrA [X in _ * X]mulrC.
-by rewrite divff ?natmul_inj // mulr1.
+move=> f g f0_eq0 g0_eq0 /=.
+rewrite !exp_coef0_eq0 ?rpredD //.
+pose FG u v := (u`! * v`!)%:R ^-1 *: (g ^+ u * f ^+ v) : {tfps R n}.
+rewrite (eq_bigr
+           (fun i : 'I_n.+1 => \sum_(j < i.+1) FG j (i - j)%N)); first last.
+  move => [i /= _] _; rewrite exprDn.
+  rewrite scaler_sumr; apply: eq_bigr => [[j]]; rewrite /= ltnS => le_ji _.
+  rewrite mulrC -mulrnAl scalerAl -scaler_nat scalerA -scalerAl; congr(_ *: _).
+  case: i le_ji => [|i le_ji1].
+    by rewrite leqn0 => /eqP ->; rewrite fact0 bin0 mulr1 muln1.
+  rewrite bin_factd //.
+  rewrite natr_div ?mulKr ?fact_unit // ?natrM ?unitrM ?fact_unit //.
+  by apply/dvdnP; exists 'C(i.+1, j); rewrite bin_fact.
+rewrite -(triangular_index_bigop _ FG (ltnSn n)) /= {}/FG.
+rewrite mulrC (big_distrl _ _ _) /=; apply eq_bigr => i _.
+rewrite [RHS]mulr_sumr [RHS](bigID (fun j : 'I_n.+1 => i + j < n.+1)) /=.
+rewrite [X in _ + X]big1 ?addr0; first last.
+  move => j; rewrite -ltnNge ltnS => lt_nij.
+  by rewrite -scalerAr -scalerAl tfpsMX_eq0 // !scaler0.
+apply eq_bigr => j _.
+by rewrite -scalerAr -scalerAl scalerA natrM invrM // fact_unit.
 Qed.
 
-Lemma coef0_prim_tfps (p : tfps K n) : (prim_tfps p)`_0 = 0.
-Proof. by rewrite coef_poly eqxx mulr0n invr0 mulr0. Qed.
-
-Lemma deriv_tfpsK : 
-    {in @coef0_is_0 K n.+1, cancel (@deriv_tfps _ _) (@prim_tfps _)}.
+Lemma expN f : f \in coef0_eq0 -> exp (- f) = (exp f)^-1.
 Proof.
-move=> f; rewrite coef0_is_0E => /eqP f0_eq0.
-apply/val_inj; apply/polyP => i; rewrite coef_poly.
-have [|/leq_sizeP big_i] := ltnP; last by rewrite big_i // size_tfps.
-case: i => [_|i]; first by rewrite eqxx mulr0n mul0r f0_eq0.
-rewrite ltnS => small_i; rewrite coef_poly small_i -lt0n ltn0Sn -mulr_natr mulr1.
-by rewrite -mulr_natr -mulrA divff ?natmul_inj // mulr1.
+move=> f0_eq0; apply: (@mulrI _ (exp f)); rewrite ?divrr ?exp_unit //.
+by rewrite -expD ?rpredN // subrr exp0.
 Qed.
 
-End Primitive.
+Lemma expB : {in (@coef0_eq0 R n) &, {morph exp : f g / f - g >-> f / g}}.
+Proof. by move=> f g hf hg; rewrite expD ?rpredN // expN. Qed.
 
-Section Composition.
+End ExpMorph.
 
-Variables (K : fieldType) (n : nat).
-  
-Definition comp_tfps m (g p : {tfps K m}) :=
-  if g \in (@coef0_is_0 K m) then Tfpsp m (comp_poly g p) else 0.
 
-Local Notation "f \So g" := (comp_tfps g f) (at level 2) : tfps_scope. 
+Section MoreDerivative.
 
-Lemma comp_tfps_coef0_neq0 (f g : {tfps K n}) :
-                                       g \notin (@coef0_is_0 K n) -> f \So g = 0.
-Proof. by move/negbTE => p0_neq0; rewrite /comp_tfps p0_neq0. Qed.
+Variable R : comUnitRingType.
+Hypothesis nat_unit : forall i, i.+1%:R \is a @GRing.unit R.
+Variable n : nat.
 
-Lemma comp_tfps_coef0_eq0 (f g : {tfps K n}) :
-                g \in (@coef0_is_0 K n) -> f \So g = Tfpsp n (comp_poly g f).
-Proof. by move => f0_eq0 ; rewrite /comp_tfps f0_eq0. Qed.
+Implicit Types (f g : {tfps R n}).
 
-Section Variable_f.
+Theorem derivXn_tfps m :
+  m != 0%N ->  {in GRing.unit, forall f,
+     (f ^- m)^`() = (trXnt n.-1 f) ^- m.+1 * f^`()%tfps *- m}.
+Proof.
+move=> Hm /= f fU; rewrite -exprVn derivX_tfps derivV_tfps //.
+rewrite rmorphV ?leq_pred //= => _.
+rewrite !exprVn rmorphX ?leq_pred //= => _.
+rewrite [_/_]mulrC mulrA mulrN mulNrn -!mulrnAr.
+rewrite -!exprVn -exprD -addSnnS addn1.
+by case: m Hm.
+Qed.
 
-Variable (f : {tfps K n}).
+Lemma deriv_tfps_eq0_cst f : f^`() = 0 -> {c : R | f = c %:S}.
+Proof.
+move: f; case: n => [f _| m f H]; exists (f`_0).
+  by rewrite {1}[f]tfps_is_cst.
+apply/tfpsP => [] [|i]; rewrite coef_tfpsC // ltnS [RHS]/= => le_im.
+apply: (mulIr (nat_unit i)); rewrite mul0r.
+move: H => /(congr1 (fun x : {tfps _ _ } => x`_i)).
+by rewrite coef_deriv_tfps coef0 -mulr_natr.
+Qed.
 
-Lemma comp_tfps0r : f \So 0 = (f`_0) %:S.
-Proof. by rewrite comp_tfps_coef0_eq0 ?rpred0 // comp_poly0r. Qed.
+Lemma deriv_tfps_ex_eq0 f :
+  f^`() = 0 -> {x : R | (tfps f).[x] = 0} -> f = 0.
+Proof.
+move=> /deriv_tfps_eq0_cst [c ->] [x].
+rewrite val_tfpsC /= hornerC => ->.
+by rewrite tfpsC0.
+Qed.
 
-Lemma comp_tfpsr0 : 0 \So f = 0.
+Lemma deriv_tfps_eq0 f : f^`() = 0 -> f`_0 = 0 -> f = 0.
 Proof.
-have [f0_eq0 | f0_neq0] := boolP (f \in (@coef0_is_0 K n)).
-+ by rewrite comp_tfps_coef0_eq0 // comp_poly0 rmorph0.
-+ by rewrite comp_tfps_coef0_neq0.
+move=> /deriv_tfps_ex_eq0 H f0_eq0; apply: H.
+by exists 0; rewrite horner_coef0.
 Qed.
 
-(* is there a better statement ? *)
-Lemma comp_tfpsC (c : K) : c%:S \So f = (c * (f \in (@coef0_is_0 K n))%:R) %:S.
+Lemma deriv_tfps_ex_eq f g :
+  f^`() = g^`() -> {x : R | (tfps f).[x] = (tfps g).[x]} -> f = g.
 Proof.
-have [f0_eq0 | f0_neq0] := boolP (f \in (@coef0_is_0 K n)).
-+ by rewrite comp_tfps_coef0_eq0 //= modCXn // comp_polyC mulr1.
-+ by rewrite mulr0 Tfpsp0 comp_tfps_coef0_neq0.
+move=> H [x Hx].
+apply/eqP; rewrite -(subr_eq0 f g); apply/eqP.
+apply: deriv_tfps_ex_eq0; first by rewrite linearB /= H subrr.
+by exists x ; rewrite -horner_evalE rmorphB /= horner_evalE Hx subrr.
 Qed.
 
-Lemma comp_tfpsCf (c : K) : f \So (c%:S) = (f`_0 * (c == 0)%:R) %:S.
+Lemma deriv_tfps_eq f g : f^`() = g^`() -> f`_0 = g`_0 -> f = g.
 Proof.
-have [->| /negbTE c_neq0] := eqVneq c 0.
-  by rewrite eqxx mulr1 rmorph0 comp_tfps0r.
-rewrite comp_tfps_coef0_neq0; last first.
-  by rewrite coef0_is_0E nth0_Tfpsp coefC eqxx negbT.
-by rewrite c_neq0 mulr0 rmorph0.
+move=> /deriv_tfps_ex_eq H Heq0; apply: H.
+by exists 0; rewrite !horner_coef0.
 Qed.
 
-Hypothesis (f0_is_0 : f \in (@coef0_is_0 K n)).
+End MoreDerivative.
+
+
+Section DerivExpLog.
+
+Variables R : comUnitRingType.
+Hypothesis nat_unit : forall i, i.+1%:R \is a @GRing.unit R.
+Variable n : nat.
+Implicit Types (f g : {tfps R n}).
+
 
-Fact comp_tfps_is_additive : additive (comp_tfps f).
+Theorem deriv_exp f : (exp f)^`() = f^`()%tfps * trXnt n.-1 (exp f).
 Proof.
-move => u v; rewrite !comp_tfps_coef0_eq0 //.
-by apply/val_inj; rewrite rmorphB /= modp_add modNp.
+case: n f => /= [| m] f.
+  by rewrite [f]tfps_is_cst deriv_tfpsC mul0r expC deriv_tfpsC.
+case: (boolP (f \in coef0_eq0)) => [p0_eq0 | p0_neq0]; last first.
+  by rewrite exp_coef0_isnt_0 // deriv_tfps0 rmorph0 // mulr0.
+rewrite !exp_coef0_eq0 //.
+rewrite raddf_sum /= -(big_mkord predT (fun i => i`!%:R^-1 *: _  ^+ i)) /=.
+rewrite big_nat_recr //= rmorphD linearZ /=.
+rewrite rmorphX tfpsX_eq0 ?coef0_eq0_trXnt // scaler0 addr0.
+rewrite rmorph_sum mulr_sumr /=.
+rewrite -(big_mkord predT (fun i => (i`!%:R^-1 *: f ^+ i)^`())) /=.
+rewrite big_nat_recl // expr0 linearZ /= deriv_tfps1 scaler0 add0r.
+apply: eq_bigr => i _.
+rewrite !linearZ -scalerCA /= derivX_tfps.
+rewrite -scaler_nat scalerA /= rmorphX /= -scalerAl [f^`()%tfps * _]mulrC.
+congr (_ *: _).
+rewrite factS natrM /= invrM ?fact_unit //.
+by rewrite -mulrA [X in _ * X]mulrC divrr // mulr1.
 Qed.
 
-Fact comp_tfps_is_linear : linear (comp_tfps f).
+Theorem deriv_log f :
+  f \in coef0_eq1 -> (log f)^`() = f^`()%tfps / trXnt n.-1 f.
 Proof.
-move => a q r.
-by rewrite !comp_tfps_coef0_eq0 // !rmorphD /= modp_scalel mod_tfps // !linearZ.
+case: n f => [|m] f.
+  rewrite [f]tfps_is_cst coef0_eq1E coef_tfpsC => /eqP ->.
+  by rewrite !deriv_tfps0p mul0r.
+move => f0_eq1.
+rewrite log_coef0_eq1 //.
+rewrite !raddf_sum /= big_nat.
+rewrite (eq_bigr (fun i => f^`()%tfps * ((1 - trXnt m f) ^+ i.-1))) =>
+                                                  [|i /andP [hi _]]; last first.
+- rewrite linearN linearZ /= derivX_tfps /=.
+  rewrite -scaler_nat scalerA mulrC divrr; last by case: i hi.
+  rewrite scale1r !linearD /= deriv_tfps1 add0r !linearN /=.
+  by rewrite mulrN opprK trXnt1 mulrC.
+- rewrite -big_nat /= -mulr_sumr big_add1 /= big_mkord; congr (_ * _).
+  have tfps_unit : trXnt m f \is a GRing.unit.
+    by rewrite trXn_unitE -unit_tfpsE coef0_eq1_unit.
+  apply: (mulrI tfps_unit); rewrite divrr //.
+  rewrite -[X in X * _]opprK -[X in X * _]add0r -{1}(subrr 1).
+  rewrite -addrA -linearB /= -[X in X * _]opprB mulNr -subrX1 opprB /=.
+  rewrite tfpsX_eq0 ?subr0 //.
+  by rewrite -coef0_eq10 coef0_eq1_trXnt.
 Qed.
 
-End Variable_f.
-End Composition.
-
-Section MoreComposition.
+Lemma expK : {in coef0_eq0, cancel (@exp R n) (@log R n)}.
+Proof.
+move => f f0_eq0 /=.
+apply/eqP; rewrite -(subr_eq0 _ f); apply/eqP.
+apply: (deriv_tfps_eq0 nat_unit).
+- rewrite linearB /= deriv_log ?exp_in_coef0_eq1 //.
+  rewrite deriv_exp // -mulrA divrr ?mulr1 ?subrr // trXn_unitE.
+  by rewrite coef0_exp // unitr1.
+- by rewrite coefB coef0_log (eqP f0_eq0) subrr.
+Qed.
 
-Local Notation "f \So g" := (comp_tfps g f) (at level 2) : tfps_scope.
+Lemma exp_inj : {in coef0_eq0 &, injective (@exp R n)}.
+Proof. exact: (can_in_inj expK). Qed.
 
-Local Notation "f ^` () " := (deriv_tfps f) (at level 8) : tfps_scope.
+Lemma log_inj : {in coef0_eq1 &, injective (@log R n)}.
+Proof.
+move=> f g f0_eq0 g0_eq0 /= Hlog.
+have {Hlog} : (f / g)^`() = 0.
+  rewrite deriv_div_tfps; last exact: coef0_eq1_unit.
+  rewrite [X in X / _](_ : _ = 0) ?mul0r //.
+  apply/eqP; rewrite subr_eq0 [X in _ == X]mulrC.
+  rewrite -eq_divr ?trXnt_unitE -?unit_tfpsE ?coef0_eq1_unit //.
+  by move/(congr1 (@deriv_tfps R n)): Hlog; rewrite !deriv_log // => ->.
+move/(deriv_tfps_eq0_cst nat_unit) => [c Hpq].
+suff Hc : c = 1 by subst c; move: Hpq; rewrite tfpsC1; apply: divr1_eq.
+move/(congr1 (fun x => x * g)): Hpq.
+rewrite mulrAC -mulrA divrr ?trXnt_unitE -?unit_tfpsE ?coef0_eq1_unit //.
+rewrite mulr1 -alg_tfpsC mulr_algl=> /(congr1 (fun x : {tfps R n} => x`_0)).
+rewrite coefZ.
+move: f0_eq0 g0_eq0; rewrite !coef0_eq1E => /eqP -> /eqP ->.
+by rewrite mulr1 => ->.
+Qed.
 
-Lemma deriv_tfps_comp (K : fieldType) (m : nat) (f g : {tfps K m}): 
-  f \in (@coef0_is_0 K m) ->
-  deriv_tfps (g \So f) = (g ^`() \So (Tfpsp m.-1 f)) * f^`()%tfps.
+Lemma logK : {in coef0_eq1 , cancel (@log R n) (@exp R n)}.
 Proof.
-rewrite !deriv_tfpsE //.
-move: f g; case: m => [f g g0_eq0| m f g g0_eq0].
-+ apply/val_inj => /=.
-  rewrite [f]tfps_is_cst [g]tfps_is_cst Tfpsp_Tfpsp // comp_tfpsC !deriv_modp.
-  by rewrite !derivC !mod0p mulr0 mod0p.
-+ rewrite /= comp_tfps_coef0_eq0 // comp_tfps_coef0_eq0 ?p0_is_0; last first.
-    by rewrite coef0_is_0E nth0_Tfpsp -coef0_is_0E.
-  apply/val_inj => /=.
-  rewrite deriv_modp deriv_comp modp_mod modp_mul.
-  rewrite mulrC -[LHS]modp_mul mulrC; congr (modp _) ; congr (_ * _). 
-  rewrite [deriv g %% 'X^m.+1]modp_small ; last first.
-  rewrite size_polyXn (leq_ltn_trans (leq_size_deriv _)) //.
-  have [-> //|] := eqVneq (size g) 0%N.
-  by rewrite -lt0n => sp_gt0; rewrite prednK // size_tfps.
-  rewrite (divp_eq (val f) 'X^m.+1) modp_add modp_mull add0r modp_mod.
-  rewrite !comp_polyE !modp_sumn /=; apply: eq_bigr => i _.
-  rewrite !modp_scalel; congr (_ *: _).
-  rewrite exprDn big_ord_recr /= subnn expr0 mul1r binn mulr1n modp_add.
-  rewrite modp_sumn /= (eq_bigr (fun j => 0)) => [|j _].
-    by rewrite big1_eq add0r.
-  rewrite -scaler_nat modp_scalel; apply/eqP.
-  rewrite scaler_eq0 ; apply/orP; right.
-  apply/eqP; apply: modp_eq0.
-  by rewrite dvdp_mulr // exprMn dvdp_mull // dvdp_exp // subn_gt0.
-Qed.
-
-End MoreComposition.
-
-Section Exponential.
-
-Variables (K : fieldType) (m : nat).
-
-Lemma expr_coef0_is_0 (n : nat) : m < n -> 
-    {in @coef0_is_0 K m, forall f, f^+n = 0}.
-Proof.
-move => lt_mn f; rewrite coef0_is_0E; move/eqP.
-rewrite -horner_coef0 => /polyXsubCP p0_eq0.
-rewrite polyC0 subr0 in p0_eq0; apply/val_inj => /=.
-rewrite val_exp_tfps; apply/modp_eq0P.
-by rewrite (dvdp_trans (dvdp_exp2l ('X : {poly K}) lt_mn)) // dvdp_exp2r.
-Qed.
-
-(* to generalize *)
-Lemma coef0_1subf_is_0 f :
-  f \in (@coef0_is_1 K m) -> (1 - f) \in (@coef0_is_0 K m).
-Proof.
-rewrite ?coef0_is_0E ?coef0_is_1E.
-rewrite -!horner_coef0 -!horner_evalE rmorphB /= !horner_evalE hornerC.
-by move=> /eqP -> ; rewrite subrr.
-Qed.
-
-Lemma exp_coef0_is_0 f : f \in @coef0_is_0 K m ->
-  exp f = Tfpsp m (\sum_(i < m.+1) ((i`! %:R) ^-1) *: ((val f) ^+i)).
-Proof. by rewrite /exp => ->. Qed.
+move=> f f0_eq1 /=.
+apply: log_inj => //; first by rewrite exp_in_coef0_eq1 log_in_coef0_eq0.
+by rewrite expK // log_in_coef0_eq0.
+Qed.
 
-Lemma exp_coef0_isnt_0 f : f \notin @coef0_is_0 K m -> exp f = 0.
-Proof. by rewrite /exp => /negPf ->. Qed.
+Lemma logM : {in coef0_eq1 &, {morph (@log R n) : f g / f * g >-> f + g}}.
+Proof.
+move=> f g f0_eq1 g0_eq1 /=.
+apply exp_inj; rewrite ?rpredD ?log_in_coef0_eq0 //.
+rewrite expD ?log_in_coef0_eq0 //.
+by rewrite !logK // rpredM.
+Qed.
 
-Lemma exp0: exp (0 : {tfps K m}) = 1.
+Lemma logV : {in coef0_eq1, {morph (@log R n) : f / f^-1 >-> - f}}.
 Proof.
-apply/val_inj/polyP=> j.
-rewrite exp_coef0_is_0 ?rpred0 //=.
-rewrite (eq_bigr (fun i => ((nat_of_ord i) == O)%:R))=> [|i]; last first.
-  by case: (_ i) => [|k]; rewrite expr0n ?eqxx ?fact0 ?invr1 ?scale1r ? scaler0.
-rewrite -(big_mkord predT (fun i => (i == _)%:R)) /=.
-rewrite big_ltn // eqxx big_nat /= big1 => [|i /andP [hi _]]; last first.
-  by rewrite eqn0Ngt hi.
-by rewrite addr0 modCXn.
+move=> f f0_eq1 /=.
+apply exp_inj; rewrite ?rpredN ?log_in_coef0_eq0 //.
+rewrite expN ?log_in_coef0_eq0 //.
+by rewrite !logK // rpredV.
 Qed.
 
-Lemma expC (c : K) : exp (c %:S) = (c == 0)%:R %:S :> {tfps K m}.
+Lemma log_div : {in coef0_eq1 &, {morph (@log R n) : f g / f / g >-> f - g}}.
+Proof. by move=> f g f0_eq1 g0_eq1 /=; rewrite logM ?rpredV // logV. Qed.
+
+
+Section ExprTfps.
+
+Variable f : {tfps R n}.
+Hypothesis f0_eq1 : f \in coef0_eq1.
+
+Let log_coef0_eq0Z c : c *: log f \in coef0_eq0.
+Proof. by rewrite coef0_eq0Z // log_in_coef0_eq0. Qed.
+
+Lemma coef0_eq1_expr c : f ^^ c \in coef0_eq1.
+Proof. by rewrite /expr_tfps exp_in_coef0_eq1 log_coef0_eq0Z. Qed.
+
+Lemma expr_tfpsn m : f ^^ m%:R = f ^+ m.
 Proof.
-have [p0eq0 | p0N0] := boolP (c %:S \in @coef0_is_0 K m).
-+ rewrite coef0_is_0E nth0_Tfpsp coefC /= in p0eq0.
-  move: p0eq0 => /eqP p0eq0.
-  rewrite p0eq0 eqxx exp_coef0_is_0 //=; last by rewrite rmorph0 rpred0.
-  rewrite mod0p -(big_mkord predT (fun i => i`!%:R^-1 *: 0%:P ^+ i)) /=.
-  rewrite big_ltn // fact0 expr0 invr1 big_nat_cond.
-  rewrite (eq_bigr (fun i => 0))=> [ | i /andP [/andP [Hi _] _] ] ; last first.
-    by rewrite expr0n eqn0Ngt Hi /= scaler0.
-  by rewrite scale1r big1_eq addr0.
-+ rewrite exp_coef0_isnt_0 //.
-  rewrite coef0_is_0E nth0_Tfpsp coefC /= in p0N0.
-  by move/negbTE: p0N0 => ->; rewrite rmorph0.
+rewrite /expr_tfps; elim: m => [|m IHm]; first by rewrite expr0 scale0r exp0.
+rewrite -{1}add1n natrD scalerDl scale1r expD ?log_in_coef0_eq0 //.
+by rewrite {}IHm logK // exprS.
 Qed.
 
-Hypothesis char_K_is_zero : [char K] =i pred0.
+Lemma expr_tfps1 : f ^^ 1 = f.
+Proof. by rewrite -[1]/(1%:R) expr_tfpsn expr1. Qed.
 
-Lemma exp_is_morphism :
-            {in (@coef0_is_0 K m) &, {morph (@exp _ _) : f g / f + g >-> f * g}}.
-Proof.
-move => f g f0_eq0 g0_eq0 /=.
-rewrite ?(exp_coef0_is_0, rpredD) //.
-apply/val_inj => /=; apply/val_inj => /=.
-rewrite modp_mul mulrC modp_mul -mulrC.
-rewrite coef0_is_0E -!horner_coef0 in f0_eq0 g0_eq0.
-move/eqP: g0_eq0 ; move/eqP : f0_eq0.
-move: f g => [f fr] [g gr] /=.
-rewrite !horner_coef0 => f0_eq0 g0_eq0.
-rewrite (eq_bigr (fun i => let i' := (nat_of_ord i) in i'`!%:R^-1 *:
-         (\sum_(j < i'.+1) f ^+ (i' - j) * g ^+ j *+ 'C(i', j)))); last first.
-  by move => i _ ; rewrite exprDn.
-rewrite (big_distrl _ _ _) /=.
-rewrite (eq_bigr (fun i => let i' := (nat_of_ord i) in (\sum_(j < i' .+1)
-        ((j`! * (i' -j)`!)%:R) ^-1 *: (f ^+ (i' - j) * g ^+ j)))); last first.
-  move => [i i_lt_Sn] _ /=.
-  rewrite scaler_sumr; apply: eq_bigr => [ /= [j j_lt_Si]] _ /=.
-  rewrite -mulrnAl scalerAl -scaler_nat scalerA -scalerAl; congr(_ *: _).
-  have factr_neq0 k : k`!%:R != 0 :> K.
-    by rewrite (proj1 (charf0P _)) // -lt0n fact_gt0.
-  apply: (mulfI (factr_neq0 i)); rewrite mulVKf //.
-  have den_neq0 :  (j`! * (i - j)`!)%:R != 0 :> K by rewrite natrM mulf_neq0.
-  by apply: (mulIf den_neq0) ; rewrite mulfVK // -natrM bin_fact.
-rewrite [in RHS](eq_bigr (fun i => let i' := (nat_of_ord i) in (\sum_(j < m.+1)
-                    ((i'`! * j`!)%:R^-1) *: (f ^+ i' * g ^+ j)))); last first.
-  move => i _.
-  rewrite (big_distrr _ _ _) /=.
-  apply: eq_bigr => j _ /=.
-  rewrite -scalerAl -scalerCA -scalerAl scalerA -invrM ?unitfE; last 2 first.
-  + move/(charf0P K)/(_ (j`!)%N) : char_K_is_zero ->.
-    by rewrite -lt0n fact_gt0.
-  + move/(charf0P K)/(_ (i`!)%N) : char_K_is_zero ->.
-    by rewrite -lt0n fact_gt0.
-  by rewrite -natrM mulnC.
-have -> : (\sum_(i < m.+1) \sum_(j < m.+1)
-  (i`! * j`!)%:R^-1 *: (f ^+ i * g ^+ j)) %% 'X^m.+1 =
-  (\sum_(i < m.+1) \sum_(j < m.+1 | i+j <= m)
-  (i`! * j`!)%:R^-1 *: (f ^+ i * g ^+ j)) %% 'X^m.+1.
-  rewrite !modp_sumn ; apply: eq_bigr => [[i i_lt_Sn]] _ /=.
-  rewrite !modp_sumn.
-  rewrite (bigID (fun j => i + (nat_of_ord j) <= m)) /=.
-  rewrite -[RHS]addr0 ; congr (_ + _).
-  rewrite -(big_mkord (fun j => ~~ (i + j <= m))
-                      (fun j => ((i`! * j`!)%:R^-1 *: (f ^+ i * g ^+ j)) %% 'X^m.+1)).
-  apply: big1_seq => /= n.
-  rewrite -ltnNge ; move/andP => [ n_lt_addim _].
-  apply/modp_eq0P.
-  rewrite dvdp_scaler ; last first.
-  rewrite invr_eq0.
-    move/(charf0P K)/(_ (i`! * n`!)%N) : char_K_is_zero ->.
-    by rewrite muln_eq0 negb_or -!lt0n !fact_gt0.
-    rewrite (dvdp_trans (dvdp_exp2l ('X : {poly K}) n_lt_addim)) // exprD.
-    by rewrite dvdp_mul // dvdp_exp2r // ; apply/polyXP.
-apply: (congr1 (fun x => polyseq x)).
-apply: (congr1 (fun x => modp x (GRing.exp (polyX K) (S m)))).
-rewrite [in RHS](eq_bigr (fun i => let i' := (nat_of_ord i) in \sum_(j < m.+1 |
-        i' + j < m.+1) (i'`! * j`!)%:R^-1 *: (f ^+ i' * g ^+ j))); last first.    
-  move => i _.
-  by apply: eq_bigr.
-rewrite (eq_bigr (fun i => let i' := (nat_of_ord i) in \sum_(j < i'.+1)
-           (j`! * (i' - j)`!)%:R^-1 *: (f ^+ j * g ^+ (i' - j)))); last first.
-  move => i _.
-  rewrite /=.
-  rewrite -(big_mkord predT (fun j => (j`! * (i - j)`!)%:R^-1 *: 
-                                                       (f ^+ (i - j) * g ^+ j))).
-  rewrite big_nat_rev big_mkord add0n.
-  apply: eq_bigr => j _.
-  by rewrite !subSS subnBA -1?ltnS // !addKn mulnC.
-by rewrite (triangular_index_bigop _
-                      (fun i j => (i`! * j`!)%:R^-1 *: (f ^+ i * g ^+ j))) /=;
-  last exact: ltnSn.
-Qed.
-
-Lemma log_coef0_is_1 f : f \in @coef0_is_1 K m ->
-  log f = Tfpsp m (- \sum_(1 <= i < m.+1) ((i %:R) ^-1) *: ((1 - (val f)) ^+i)).
-Proof. by rewrite /log => ->. Qed.
+Lemma expr_tfps0 : f ^^ 0 = 1.
+Proof. by rewrite -[0]/(0%:R) expr_tfpsn expr0. Qed.
 
-Lemma log_coef0_isnt_1 f : f \notin @coef0_is_1 K m -> log f = 0.
-Proof. by rewrite /log => /negPf ->. Qed.
+Lemma expr_tfpsN a : f ^^ (- a) = (f ^^ a)^-1.
+Proof. by rewrite /expr_tfps scaleNr expN. Qed.
+
+Lemma expr_tfpsN1 : f ^^ (-1) = f ^-1.
+Proof. by rewrite expr_tfpsN expr_tfps1. Qed.
+
+Lemma expr_tfpsD a b : f ^^ (a + b) = (f ^^ a) * (f ^^ b).
+Proof. by rewrite /expr_tfps scalerDl expD. Qed.
+
+Lemma expr_tfpsB a b : f ^^ (a - b) = (f ^^ a) / (f ^^ b).
+Proof. by rewrite expr_tfpsD expr_tfpsN. Qed.
+
+Lemma expr_tfpsM a b : f ^^ (a * b) = (f ^^ a) ^^ b.
+Proof. by rewrite /expr_tfps expK ?scalerA ?[b * a]mulrC. Qed.
+
+Lemma deriv_expr_tfps a :
+  (f ^^ a)^`() = a *: trXnt n.-1 (f ^^ (a - 1)) * f^`()%tfps.
+Proof.
+rewrite {1}/expr_tfps deriv_exp -/(f ^^ a).
+rewrite linearZ /= deriv_log // -!scalerAl; congr (_ *: _).
+rewrite -mulrA mulrC; congr (_ * _).
+rewrite -trXntV ?leq_pred // -rmorphM ?leq_pred //= => _.
+by rewrite mulrC expr_tfpsB expr_tfps1.
+Qed.
 
-Lemma log1 : log (1 : {tfps K m}) = 0.
+End ExprTfps.
+
+Lemma expr_tfpsNn f m : f \in coef0_eq1 -> f ^^ (-m%:R) = f ^- m.
 Proof.
-apply/val_inj/polyP=> j; rewrite log_coef0_is_1 ?rpred1 // coef0 coef_Tfpsp.
-case: ifP => // j_small; rewrite coefN big1 ?coef0 ?oppr0 //.
-by move=> [|i]; rewrite subrr expr0n ?eqxx ?invr0 ?scale0r ?scaler0.
+move=> Hf.
+by rewrite -mulN1r expr_tfpsM expr_tfpsN1 ?expr_tfpsn ?exprVn ?rpredV.
 Qed.
 
-(* is there a better statement ? something like: *)
-(* Lemma coef0_exp f : (exp f)`_0 = (f \notin coef0_is_0)%:R. *)
-Lemma coef0_exp f : f \in @coef0_is_0 K m -> (exp f)`_0 = 1.
+Lemma expr_tfpsK a : a \is a GRing.unit ->
+  {in coef0_eq1, cancel (@expr_tfps R n a) (@expr_tfps R n a^-1)}.
+Proof. by move=> aU f f0_eq1; rewrite -expr_tfpsM divrr ?expr_tfps1. Qed.
+
+Lemma expr_tfps_inj a : a \is a GRing.unit ->
+  {in coef0_eq1 &, injective (@expr_tfps R n a)}.
+Proof. by move=> /expr_tfpsK/can_in_inj. Qed.
+
+
+Local Notation "\sqrt f" := (f ^^ (2%:R^-1)).
+
+Lemma sqrrK f : f \in coef0_eq1 -> \sqrt (f ^+ 2) = f.
 Proof.
-move => f0_eq0.
-rewrite exp_coef0_is_0 // coef_modXn ltn0Sn -horner_coef0.
-rewrite -horner_evalE rmorph_sum /=.
-rewrite (eq_bigr (fun i => ((nat_of_ord i) == 0%N)%:R)) => [ | [i _] _ ] /=.
-+ rewrite -(big_mkord predT (fun i => ((i == _)%:R))) big_ltn ?ltnS //. 
-  rewrite eqxx /= -natr_sum big_nat_cond.
-  rewrite (eq_big (fun i => (0 < i < m.+1)) (fun i => 0%N)) => [ | i | i ].
-- by rewrite big1_eq addr0.
-- by rewrite andbT.
-  by rewrite andbT => /andP [/lt0n_neq0/negbTE -> _].
-+ rewrite linearZ /= rmorphX /= horner_evalE horner_coef0.
-  move: f0_eq0 ; rewrite coef0_is_0E => /eqP ->.
-  rewrite expr0n ; case: i => [ | i'].
-- by rewrite fact0 invr1 mul1r.
-- by rewrite eqn0Ngt -leqNgt ltn0 mulr0.
+by move => Hh; rewrite -expr_tfpsn -?expr_tfpsM ?divrr ?expr_tfps1.
 Qed.
 
-Lemma coef0_log (f : {tfps K m}) : (log f)`_0 = 0.
+Lemma sqrtK f : f \in coef0_eq1 -> (\sqrt f) ^+ 2 = f.
 Proof.
-have [f0_eq1|f0_neq1] := boolP (f \in @coef0_is_1 K m); last first.
-  by rewrite log_coef0_isnt_1 // coefC.
-rewrite log_coef0_is_1 // coef_modXn ltn0Sn -horner_coef0.
-rewrite -horner_evalE rmorphN rmorph_sum /=.
-rewrite big_nat_cond (eq_bigr (fun i => (i == 0%N)%:R)).
-+ rewrite -[1%N]add0n big_addn (eq_bigr (fun i => 0)) => [ | i _]; last first.
-    by rewrite addn1.
-  by rewrite big1_eq oppr0.
-+ move => i /andP [/andP [Hi _] _] /=.
-  rewrite linearZ rmorphX rmorphB /= !horner_evalE hornerC horner_coef0.
-  move: f0_eq1 ; rewrite coef0_is_1E => /eqP ->.
-  by rewrite subrr expr0n eqn0Ngt Hi /= mulr0.
+move => Hh; rewrite -expr_tfpsn ?coef0_eq1_expr //.
+by rewrite -?expr_tfpsM // mulrC divrr ?expr_tfps1.
 Qed.
 
-End Exponential.
+End DerivExpLog.
+
+Notation "\sqrt f" := (f ^^ (2%:R^-1)) : tfps_scope.
 
-Section MoreExponential.
 
-Variable (K : fieldType).
+Section CoefExpX.
 
-Local Notation "f ^` ()" := (deriv_tfps f) (at level 8) : ring_scope. 
+Variables R : comUnitRingType.
+Hypothesis nat_unit : forall i, i.+1%:R \is a @GRing.unit R.
 
-Lemma deriv_tfps_exp (m : nat) (f : {tfps K m}) (n : nat) :
-    (f ^+ n)^` () = f^` () * (Tfpsp m.-1 f) ^+ n.-1 *+ n.
+Lemma coef1cX n c : 1 + c *: \Xo(n) \in @coef0_eq1 R n.
 Proof.
-elim: n => /= [|n IHn]; first by rewrite expr0 mulr0n onefE deriv_tfpsC.
-rewrite exprS deriv_tfpsM {}IHn (mulrC (_ f)) val_exp_tfps /=.
-rewrite mulrC -mulrnAr mulrCA -mulrDr -mulrnAr; congr (_ * _).
-rewrite Tfpsp_modp; last by clear f; case: m.
-rewrite rmorphX /= mulrnAr -exprS; case: n => /= [|n]; rewrite -?mulrS //.
-by rewrite !expr0 mulr0n addr0.
+rewrite coef0_eq1E coeftD coef_tfps1.
+by rewrite coeftZ coef_tfpsE val_tfpsX coefZ coefX !mulr0 addr0.
 Qed.
 
-Hypothesis char_K_is_zero : [char K] =i pred0.
-Hint Resolve char_K_is_zero.
-
-Lemma deriv_exp (m : nat) (p : {tfps K m}) : 
-  (exp p)^` () = (p^` ()) * (Tfpsp m.-1 (exp p)).
-Proof.
-move: p ; case: m => /= [p | n p]. 
-  by rewrite [p]tfps_is_cst deriv_tfpsC mul0r expC deriv_tfpsC.
-have [p0_eq0 | p0_neq0] := boolP (p \in (@coef0_is_0 K n.+1)) ; last first.
-  by rewrite exp_coef0_isnt_0 // deriv_tfps0 rmorph0 mulr0.
-rewrite !exp_coef0_is_0 //= !deriv_tfpsE //=; apply/val_inj => /=.
-rewrite deriv_modp modp_modp ?dvdp_exp2l // modp_modp ?dvdp_exp2l //.
-rewrite deriv_sum -(big_mkord predT (fun i => i`!%:R^-1 *: _  ^+ i)) /=.
-rewrite big_nat_recr //= modp_add modp_scalel.
-rewrite modX_eq0 //; last by apply/eqP; rewrite -coef0_is_0E.
-rewrite scaler0 addr0 modp_mul modp_mul2 mulr_sumr.
-rewrite -(big_mkord predT (fun i => deriv (i`!%:R^-1 *: (val p) ^+ i))) /=.
-rewrite big_nat_recl // expr0 linearZ /= derivC scaler0 add0r.
-congr (_ %% _); apply: eq_bigr => i _.
-rewrite linearZ /= deriv_exp /= -scalerCA -scaler_nat.
-rewrite scalerA -scalerAl; congr (_ *: _).
-rewrite factS natrM /= invrM ?unitfE ?natmul_inj // -?lt0n ?fact_gt0 //.
-rewrite -mulrA [X in _ * X]mulrC.
-by rewrite divff ?natmul_inj // -?lt0n ?fact_gt0 // mulr1.
-Qed.
-
-Lemma deriv_log (m : nat) (f : {tfps K m}) : 
-       f \in (@coef0_is_1 K m) -> (log f) ^` () = (f )^` () / (Tfpsp m.-1 f).
-Proof.
-move: f; case: m => [|m]; move => f.
-rewrite [f]tfps_is_cst coef0_is_1E nth0_Tfpsp coefC eqxx => /eqP ->.
-by rewrite !deriv_Tfps0p mul0r.
-move => f0_is_1.
-rewrite log_coef0_is_1 // rmorphN rmorph_sum linearN raddf_sum -sumrN. 
-rewrite big_nat.
-rewrite (eq_bigr (fun i => (f )^` () * ((1 - (Tfpsp m f)) ^+ i.-1))) => 
-                                                  [|i /andP [hi _]]; last first.
-+ rewrite linearZ rmorphX /= deriv_tfpsZ rmorphB rmorph1 deriv_tfps_exp. 
-  rewrite linearB rmorphB rmorph1 onefE /= deriv_tfpsC sub0r /= Tfpsp_modp //.
-  rewrite -scaler_nat scalerA mulrC divff ?natmul_inj //-?lt0n // scale1r mulNr.
-  rewrite  opprK; congr (_ * _); apply/val_inj => /=.
-  by rewrite modp_small // size_polyXn ltnS size_tfps.
-+ rewrite -big_nat /= -mulr_sumr big_add1 /= big_mkord; congr (_ * _).
-  have trp_unit : Tfpsp m f \is a GRing.unit.
-    rewrite Tfpsp_is_unit.
-    by move: f0_is_1 ; rewrite coef0_is_1E => /eqP -> ; rewrite oner_eq0.
-  apply: (mulrI trp_unit); rewrite divrr //.
-  rewrite -[X in X * _]opprK -[X in X * _]add0r -{1}(subrr 1).
-  rewrite -addrA -linearB /= -[X in X * _]opprB mulNr -subrX1 opprB /=.
-  apply/val_inj => /=.
-  rewrite val_exp_tfps modX_eq0 ?subr0 // coefB coef1 eqxx.
-  rewrite coef0_is_1E in f0_is_1.
-  rewrite nth0_Tfpsp; move/eqP : f0_is_1 ->.
-  by rewrite subrr.
+Lemma deriv1cX n c : (1 + c *: \Xo(n.+1))^`() = c%:S :> {tfps R n}.
+Proof.
+rewrite linearD /= deriv_tfps1 add0r linearZ /=.
+rewrite -alg_tfpsC; congr (_ *: _); apply tfps_inj.
+by rewrite (val_deriv_tfps \Xo(n.+1)) val_tfpsX scale1r derivX.
 Qed.
 
-Lemma cancel_log_exp (m : nat) : 
-    {in @coef0_is_0 K m, cancel (@exp K m) (@log K m)}.
+Theorem coef_expr1cX n c a m : m <= n ->
+  ((1 + c *: \Xo(n)) ^^ a)`_m = c ^+ m * \prod_(i < m) (a - i%:R) / m`!%:R :> R.
 Proof.
-move => f f0_eq0 /=.
-  apply/eqP ; rewrite -subr_eq0 ; apply/eqP.
-  apply: (pw_eq0 char_K_is_zero).
-- rewrite linearB /= deriv_log ?coef0_is_1E ?coef0_exp //.
-  rewrite deriv_exp -mulrA divrr ?mulr1 ?subrr // Tfpsp_is_unit.
-  by rewrite coef0_exp //; apply: oner_neq0.
-- exists 0; rewrite -horner_evalE rmorphB /= !horner_evalE !horner_coef0.
-  by rewrite coef0_log sub0r; apply/eqP; rewrite oppr_eq0 -coef0_is_0E.
-Qed.
-
-Lemma exp_inj (m : nat) : {in @coef0_is_0 K m &, injective (@exp K m)}.
-Proof.
-move => p q p0_eq0 q0_eq0 /= H.
-have : p^`()%tfps * (Tfpsp m.-1 (exp p)) = q^`()%tfps * (Tfpsp m.-1 (exp p)).
-  by rewrite {2}H -!deriv_exp H.
-move/mulIr => H_deriv; apply: pw_eq => //.
-+ apply: H_deriv.
-  by rewrite Tfpsp_is_unit coef0_exp // oner_neq0.
-+ exists 0 ; rewrite !horner_coef0.
-  by move: p0_eq0 q0_eq0 ; rewrite !coef0_is_0E => /eqP -> /eqP ->.
-Qed.
-
-Lemma log_inj (m : nat) : {in @coef0_is_1 K m &, injective (@log K m)}.
-Proof.
-move => p q p0_eq0 q0_eq0 /= Hlog.
-have H: (p/q) ^` () = 0.
-  rewrite deriv_div_tfps; last first.
-    by move: q0_eq0; rewrite coef0_is_1E => /eqP ->; apply: oner_neq0.
-  have -> : p^`()%tfps * Tfpsp m.-1 q - Tfpsp m.-1 p * q^`()%tfps = 0 ; 
-    last by rewrite mul0r.
-  apply/eqP; rewrite subr_eq0 [Tfpsp m.-1 p * q^`()%tfps]mulrC.
-  rewrite -eq_divr ?Tfpsp_is_unit ; last 2 first.
-      by move: p0_eq0; rewrite coef0_is_1E => /eqP ->; apply: oner_neq0.
-      by move: q0_eq0; rewrite coef0_is_1E => /eqP ->; apply: oner_neq0.
-  by move/(congr1 (@deriv_tfps K m)) : Hlog; rewrite !deriv_log // => ->.
-move: (pw_cst char_K_is_zero H) => [c Hpq].
-have Hc : c = 1.
-  move/(congr1 (fun x => x * q)): Hpq.
-  rewrite mulrAC -mulrA divrr ; last first.
-    rewrite unit_tfpsE.
-    rewrite coef0_is_1E in q0_eq0.
-    by move/eqP: q0_eq0 ->; apply: oner_neq0.
-  rewrite mulr1; move/val_eqP => /=.
-  rewrite modCXn // modp_small; last first.
-    rewrite mul_polyC (leq_ltn_trans (size_scale_leq _ _)) //.
-    by rewrite size_polyXn; apply: size_tfps.
-  move/eqP; move/(congr1 (fun x => x.[0])).
-  rewrite !horner_coef0 coef0M.
-  move: p0_eq0; rewrite coef0_is_1E => /eqP ->.
-  move: q0_eq0; rewrite coef0_is_1E => /eqP ->.
-  by rewrite coefC eqxx mulr1.
-move: Hpq; rewrite Hc; move/(congr1 (fun x => x * q)).
-rewrite mulrAC -mulrA divrr ; last first.
-  rewrite unit_tfpsE.
-  rewrite coef0_is_1E in q0_eq0.
-  by move/eqP: q0_eq0 ->; apply: oner_neq0.
-rewrite mulr1; move/val_eqP => /=.
-rewrite modp_mul2 mul1r modp_small //; last first.
-  by rewrite size_polyXn; apply: size_tfps.
-by move/eqP => H2; apply/val_inj.
-Qed.
-
-Lemma cancel_exp_log (m : nat) : {in @coef0_is_1 K m, cancel (@log K m) (@exp K m)}.
-Proof.
-move => p p0_eq1 /=.
-apply: log_inj => //.
-  rewrite coef0_is_1E.
-  apply/eqP; rewrite coef0_exp //.
-  by rewrite coef0_is_0E; apply/eqP; rewrite coef0_log.
-by rewrite cancel_log_exp // coef0_is_0E coef0_log.
-Qed.
-
-End MoreExponential.
+elim: m n a => [|m IHm] n a lt_mn.
+  rewrite big_ord0 /expr_tfps coef0_exp ?coef0_eq0Z ?log_in_coef0_eq0 //.
+  by rewrite expr0 mul1r fact0 divr1.
+case: n lt_mn => [|n] //; rewrite ltnS => le_mn.
+have:= coef_deriv_tfps ((1 + c *: \Xo(n.+1)) ^^ a) m.
+rewrite -mulr_natr => /(congr1 (fun x => x * m.+1%:R^-1)).
+rewrite mulrK // => <-.
+rewrite deriv_expr_tfps ?coef1cX // deriv1cX.
+rewrite [_ * c%:S]mulrC -alg_tfpsC mulr_algl exprS coefZ.
+rewrite coefZ coef_trXn le_mn {}IHm ?(leq_trans le_mn) // {n le_mn}.
+rewrite mulrA factS natrM invrM // ?fact_unit // !mulrA; congr (_ * _ * _).
+rewrite -[_ * a * _]mulrA [a * _]mulrC -!mulrA; congr (_ * (_ * _)).
+rewrite big_ord_recl /= subr0; congr (_ * _).
+by apply eq_bigr => i /= _; rewrite /bump /= natrD -[1%:R]/1 opprD addrA.
+Qed.
+
+Lemma coef_expr1X n a m :
+  m <= n -> ((1 + \Xo(n)) ^^ a)`_m = \prod_(i < m) (a - i%:R) / m`!%:R :> R.
+Proof.
+by move=> le_mp; rewrite -[\X]scale1r coef_expr1cX // expr1n mul1r.
+Qed.
+
+End CoefExpX.
+
+
+Section SquareRoot.
+
+Variables R : idomainType.
+Hypothesis nat_unit : forall i, i.+1%:R \is a @GRing.unit R.
+Variable n : nat.
+Implicit Types (f g : {tfps R n}).
+
+
+Lemma sqrtE f g : f \in coef0_eq1 -> g ^+ 2 = f ->
+  g = \sqrt f  \/  g = - \sqrt f.
+Proof.
+move=> /eqP f0_eq1 Heq.
+have /eqP := (congr1 (fun f : {tfps R n} => f`_0) Heq).
+rewrite -subr_eq0 {}f0_eq1 expr2 coef0_tfpsM -expr2 subr_sqr_1.
+rewrite mulf_eq0 => /orP [].
+- by rewrite subr_eq0 -coef0_eq1E -{}Heq {f} => Hg0; left; rewrite sqrrK.
+- rewrite addr_eq0 -eqr_oppLR -coefN -raddfN -coef0_eq1E -{}Heq {f} => Hg0.
+  by right; apply oppr_inj; rewrite opprK -sqrrN sqrrK.
+Qed.
+
+End SquareRoot.
+
+End TFPSUnitRing.
+
+Notation "\sqrt f" := (f ^^ (2%:R^-1)) : tfps_scope.
+
+
+Module TFPSField.
+
+Section TFPSField.
+
+Variables K : fieldType.
+Hypothesis char_K_is_zero : [char K] =i pred0.
 
+Lemma nat_unit_field i : i.+1%:R \is a @GRing.unit K.
+Proof. by rewrite unitfE; move: char_K_is_zero => /charf0P ->. Qed.
+
+Local Notation nuf := nat_unit_field.
+
+Definition natmul_inj         := TFPSUnitRing.natmul_inj         nuf.
+Definition nat_unit_alg       := TFPSUnitRing.nat_unit_alg       nuf.
+Definition fact_unit          := TFPSUnitRing.fact_unit          nuf.
+Definition pred_size_prim     := TFPSUnitRing.pred_size_prim     nuf.
+Definition primK              := TFPSUnitRing.primK              nuf.
+Definition prim_tfpsK         := TFPSUnitRing.prim_tfpsK         nuf.
+Definition deriv_tfpsK        := TFPSUnitRing.deriv_tfpsK        nuf.
+Definition derivXn_tfps       := TFPSUnitRing.derivXn_tfps.
+Definition expD               := TFPSUnitRing.expD               nuf.
+Definition expN               := TFPSUnitRing.expN               nuf.
+Definition expB               := TFPSUnitRing.expB               nuf.
+Definition deriv_tfps_eq0_cst := TFPSUnitRing.deriv_tfps_eq0_cst nuf.
+Definition deriv_tfps_ex_eq0  := TFPSUnitRing.deriv_tfps_ex_eq0  nuf.
+Definition deriv_tfps_eq0     := TFPSUnitRing.deriv_tfps_eq0     nuf.
+Definition deriv_tfps_ex_eq   := TFPSUnitRing.deriv_tfps_ex_eq   nuf.
+Definition deriv_tfps_eq      := TFPSUnitRing.deriv_tfps_eq      nuf.
+Definition deriv_exp          := TFPSUnitRing.deriv_exp          nuf.
+Definition deriv_log          := TFPSUnitRing.deriv_log          nuf.
+Definition expK               := TFPSUnitRing.expK               nuf.
+Definition exp_inj            := TFPSUnitRing.exp_inj            nuf.
+Definition logK               := TFPSUnitRing.logK               nuf.
+Definition log_inj            := TFPSUnitRing.log_inj            nuf.
+Definition logM               := TFPSUnitRing.logM               nuf.
+Definition logV               := TFPSUnitRing.logV               nuf.
+Definition log_div            := TFPSUnitRing.log_div            nuf.
+Definition coef0_eq1_expr     := TFPSUnitRing.coef0_eq1_expr.
+Definition expr_tfpsn         := TFPSUnitRing.expr_tfpsn         nuf.
+Definition expr_tfps0         := TFPSUnitRing.expr_tfps0         nuf.
+Definition expr_tfps1         := TFPSUnitRing.expr_tfps1         nuf.
+Definition expr_tfpsN         := TFPSUnitRing.expr_tfpsN         nuf.
+Definition expr_tfpsN1        := TFPSUnitRing.expr_tfpsN1        nuf.
+Definition expr_tfpsNn        := TFPSUnitRing.expr_tfpsNn        nuf.
+Definition expr_tfpsD         := TFPSUnitRing.expr_tfpsD         nuf.
+Definition expr_tfpsB         := TFPSUnitRing.expr_tfpsB         nuf.
+Definition expr_tfpsM         := TFPSUnitRing.expr_tfpsM         nuf.
+Definition sqrrK              := TFPSUnitRing.sqrrK              nuf.
+Definition sqrtK              := TFPSUnitRing.sqrtK              nuf.
+Definition coef1cX            := TFPSUnitRing.coef1cX.
+Definition deriv1cX           := TFPSUnitRing.deriv1cX.
+Definition coef_expr1cX       := TFPSUnitRing.coef_expr1cX       nuf.
+Definition coef_expr1X        := TFPSUnitRing.coef_expr1X        nuf.
+Definition sqrtE              := TFPSUnitRing.sqrtE              nuf.
+
+End TFPSField.
+
+End TFPSField.
+
+Export TFPSField.