proposition: Lemma eval_LeadCoef e p k k' : (forall x, qf_eval e (k x) = (k' (eval e x))) -> qf_eval e (LeadCoef p k) = k' (lead_coef (eval_poly e p)).
proof: Proof. move=> Pk; elim: p k k' Pk=> [|a p ihp] k k' Pk //=. by rewrite lead_coef0 Pk. rewrite (ihp _ (fun l => if l == 0 then qf_eval e (k a) else (k' l))); last first. by move=> x; rewrite eval_If /= !Pk. rewrite lead_coef_eq0; have [->|p_neq0] := altP (_ =P 0). by rewrite mul0r add0r lead_coefC. rewrite lead_coefDl ?lead_coefMX ?size_mulX // ltnS size_polyC. by rewrite (leq_trans (leq_b1 _)) // size_poly_gt0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice fintype) mathcomp(finfun path matrix) mathcomp(bigop order ssralg poly polydiv ssrnum zmodp div ssrint) mathcomp(polyorder polyrcf interval polyXY) mathcomp(qe_rcf_th ordered_qelim mxtens)