proposition: Lemma lead_coefTP (k : tF -> fF) : (forall x e, qf_eval e (k x) = qf_eval e (k (eval e x)%:T%T)) -> forall (p : polyF) (e : seq F), qf_eval e (lead_coefT p k) = qf_eval e (k (lead_coef (eval_poly e p))%:T%T).
proof: Proof. move=> kP p e; elim: p => [|a p IHp]/= in k kP e *. by rewrite lead_coef0 kP. rewrite IHp; last by move=> *; rewrite //= -kP. rewrite GRing.eval_If /= lead_coef_eq0. case p'0: (_ == _); first by rewrite (eqP p'0) mul0r add0r lead_coefC -kP. rewrite lead_coefDl ?lead_coefMX // polyseqC size_mul ?p'0 //; last first. by rewrite -size_poly_eq0 size_polyX. rewrite size_polyX addnC /=; case: (_ == _)=> //=. by rewrite ltnS lt0n size_poly_eq0 p'0. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice ssrnat seq) mathcomp(fintype generic_quotient bigop ssralg poly) mathcomp(polydiv matrix mxpoly countalg ring_quotient)