proposition: Lemma Mobius'_Xsubc_monic (c l r : R) : l != r -> l != c -> (lead_coef (Mobius' ('X - c%:P) l r))^-1 *: (Mobius' ('X - c%:P) l r) = 'X + ((r - c) / (l - c))%:P.
proof: Proof. move=> Hlr Hlc. rewrite Mobius'_Xsubc // lead_coefE. have Hlc2 : (l - c) != 0 by rewrite subr_eq0. have HlcP : ((l - c)%:P == 0) = false. apply/eqP/eqP. by rewrite polyC_eq0 subr_eq0. have Hsize : size ((l - c) *: 'X + (r - c)%:P) = 2%N. by rewrite -(mul_polyC (l - c) 'X) size_MXaddC HlcP /= size_polyC Hlc2. have Hcoef1 : ((l - c) *: 'X + (r - c)%:P)`_1 = l - c. by rewrite coefD coefC addr0 -mul_polyC coefMX coefC /=. by rewrite Hsize -mul_polyC Hcoef1 mulrDr mul_polyC -rmorphM mulrC -!mul_polyC mulrA (mulrC _ 'X) -rmorphM (mulrC _ (l - c)) mulfV //= polyC1 mulr1. Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly polydiv polyorder ssrnum zmodp) mathcomp(polyrcf qe_rcf_th complex) poly_normal pol