proposition: Lemma dc_reverse b (A B : R) p : forall i k, (i <= p)%N -> (k <= p - i)%N -> de_casteljau B A (fun t => b (p - t)%N) i k = de_casteljau A B b i (p - (i + k)).
proof: Proof. elim=> [| i ihi] k hip hk /=; first by rewrite add0n. rewrite addrC; congr (_ + _). by rewrite ihi ?(ltnW hip) ?addnS ?addSn // -[(p - i)%N]subnSK. rewrite ihi ?(leq_trans hk) // ?leq_sub2l // ?(ltnW hip) //=. rewrite addSn -subnSK //. by move:hk; rewrite -ltn_subRL -ltnS subnSK. 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