proposition: Lemma dc_delta_head : forall j k l r, (j < k)%nat -> dicho' l r (delta k) j = 0.
proof: Proof. rewrite /dicho' => j k l r hlt. pose d0 := fun _ : nat => 0 : R. rewrite (@ext_dc _ _ _ _ _ d0); last first. move=> i; rewrite add0n /delta => h1 h2. have : (i < k)%nat by apply: leq_ltn_trans hlt. by rewrite ltn_neqAle; case/andP; rewrite eq_sym; move/negPf->. elim: j {hlt} 0%nat=> [| j ihj n] /=; first by done. by rewrite !ihj !mulr0 addr0. 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