proposition: Lemma bern_rev_coef : forall (p : nat)(a b : R)(c : nat -> R), \sum_(i < p.+1) c i *: (bernp a b p i) = \sum_(i < p.+1) c (p - i)%N *: (bernp b a p i).
proof: Proof. move=> p a b c. pose t := \sum_(i < p.+1) c (p - i)%N *: bernp a b p (p - i)%N. transitivity t. by rewrite (reindex_inj rev_ord_inj) /=; apply: eq_bigl. apply:eq_bigr => [[i hi]] _ /=. by rewrite bern_swap ?subKn // leq_subr. 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