proposition: Lemma tvec_rec z q sq : tvec z (q :: sq) = castmx (erefl _, esym (exp3S _)) ( (row_mx (tvec (filter (sgp_is q 1) z) (sq)) (row_mx (tvec (filter (sgp_is q (-1)) z) (sq)) (tvec (filter (sgp_is q 0) z) (sq)))) *m (castmx (mul3n _, mul3n _) (ctmat1 *t 1%:M))).
proof: Proof. rewrite tens_ctmat1_mx !castmx_comp !castmx_id /=. rewrite !(mul_row_block, mul_row_col, mul_mx_row) !(mulmx1, mulmx0, mulmxN, addr0) /=. apply/eqP; rewrite -(can2_eq (castmxKV _ _) (castmxK _ _)); apply/eqP. apply/matrixP=> i j; rewrite !(castmxE, mxE) /=. symmetry; case: splitP=> l hl; rewrite !mxE hl. case hst: sg_tab (sg_tab_nil (size sq))=> [|s st] // _. have sst: (size st).+1 = (3 ^ size sq)%N. transitivity (size (sg_tab (size sq))); first by rewrite hst //. by rewrite size_sg_tab. rewrite /taq !big_filter !(big_mkcond (sgp_is _ _)) -sumrB. apply: congr_big=> // x _. rewrite cats0 !map_cat nth_cat !size_map /= sst ltn_ord /=. rewrite !poly_comb_cons /= !comb_expE expr1z. rewrite -!(nth_map _ 0 (fun p => p.[_])) /= ?size_map ?sst ?ltn_ord //. rewrite -!map_comp /= hornerM. set f := _ \o _; set g := _ \o _. set h := fun sc => q.[x] * (poly_comb sq sc).[x]. have hg : g =1 h. by move=> sx; rewrite /g /h /= poly_comb_cons comb_expE expr1z hornerM. rewrite -/(h _) -hg -[g _ :: _]/(map g (_ ::_)). rewrite (nth_map [::]) /= ?sst ?ltn_ord // hg /h sgzM. rewrite -![(poly_comb _ _).[_]]/(f _) -[f _ :: _]/(map f (_ ::_)). rewrite (nth_map [::]) /= ?sst ?ltn_ord // !sgr_cp0. by case: (sgzP q.[x]); rewrite ?(mul0r, mul1r, mulN1r, subr0, sub0r). case: splitP=> k hk /=; rewrite !mxE hk. case hst: sg_tab (sg_tab_nil (size sq))=> [|s st] // _. have sst: (size st).+1 = (3 ^ size sq)%N. transitivity (size (sg_tab (size sq))); first by rewrite hst //. by rewrite size_sg_tab. rewrite /taq !big_filter !(big_mkcond (sgp_is _ _)) -big_split. apply: congr_big=> // x _. rewrite cats0 !map_cat !nth_cat !size_map /= sst. rewrite ltnNge leq_addr /= addKn ltn_ord /=. rewrite !poly_comb_cons /= !comb_expE. rewrite -!(nth_map _ 0 (fun p => p.[_])) /= ?size_map ?sst ?ltn_ord //. rewrite -!map_comp /= hornerM. set f := _ \o _; set g := _ \o _. set h := fun sc => (q ^ 2).[x] * (poly_comb sq sc).[x]. have hg : g =1 h. by move=> sx; rewrite /g /h /= poly_comb_cons comb_expE hornerM. rewrite -/(h _) -hg -[g _ :: _]/(map g (_ ::_)). rewrite (nth_map [::]) /= ?sst ?ltn_ord // hg /h sgzM. rewrite -![(poly_comb _ _).[_]]/(f _) -[f _ :: _]/(map f (_ ::_)). rewrite (nth_map [::]) /= ?sst ?ltn_ord //. rewrite hornerM sgzM !sgr_cp0. by case: (sgzP q.[x]); rewrite ?(mul0r, mul1r, mulN1r, addr0, add0r). case hst: sg_tab (sg_tab_nil (size sq))=> [|s st] // _. have sst: (size st).+1 = (3 ^ size sq)%N. transitivity (size (sg_tab (size sq))); first by rewrite hst //. by rewrite size_sg_tab. rewrite /taq !big_filter !(big_mkcond (sgp_is _ _)) -!big_split. apply: congr_big=> // x _. rewrite cats0 !map_cat !nth_cat !size_map /= sst. rewrite !addKn 2!ltnNge !leq_addr /=. rewrite !poly_comb_cons /= !comb_expE expr0z mul1r. rewrite -!(nth_map _ 0 (fun p => p.[_])) /= ?size_map ?sst ?ltn_ord //. rewrite -!map_comp /=. set f := _ \o _; set g := _ \o _. have hg : g =1 f. by move=> sx; rewrite /g /f /= poly_comb_cons comb_expE expr0z mul1r. rewrite -[(poly_comb _ _).[_]]/(f _) -{4}hg. rewrite -[g s :: _]/(map _ (_ ::_)) (eq_map hg) !sgr_cp0. by case: (sgzP q.[x])=> _; rewrite ?(addr0, add0r). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq choice path fintype) mathcomp(div bigop order ssralg poly polydiv ssrnum perm zmodp ssrint) mathcomp(polyorder polyrcf interval matrix mxtens)