proposition: Lemma isol_rec_head_root : forall c l d a b q acc, q.[a] != 0 -> head_root (horner q) (isol_rec c d a b l acc).
proof: Proof. elim=> [// | c IH l d a b q acc qa0 /=]. by case tst : (changes (seqn0 l)) => [ | [ | cl]] //=; apply: IH. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat binomial seq choice order) mathcomp(fintype bigop ssralg poly ssrnum ssrint rat ssrnum) mathcomp(polyrcf qe_rcf_th realalg) pol poly_normal desc