proposition: Lemma eval_Coefs e n i : eval e (Coefs F n i) = coefs F n i.
proof: Proof. case: n => [|[|n]] //=; rewrite /coefs /=. case: i => [|i]; last first. by rewrite nth_default // size_map size_enum_ord expn0. rewrite (nth_map 0) ?size_enum_ord //. set O := _`_0; rewrite (_ : O = ord0). by rewrite ?castmxE ?cast_ord_id map_mx1 invmx1 mxE. by apply: val_inj => /=; rewrite nth_enum_ord. have [lt_i3|le_3i] := ltnP i 3; last first. by rewrite !nth_default // size_map size_enum_ord. rewrite /ctmat /= ?ntensmx1 invmx_ctmat1 /=. rewrite (nth_map 0) ?size_enum_ord // castmxE /=. rewrite !mxE !cast_ord_id //= nth_enum_ord //=. by move: i lt_i3; do 3?case. 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)