proposition: Lemma cvec_rec z q sq : cvec z (q :: sq) = castmx (erefl _, esym (exp3S _)) (row_mx (cvec (filter (sgp_is q 1) z) (sq)) (row_mx (cvec (filter (sgp_is q (-1)) z) (sq)) (cvec (filter (sgp_is q 0) z) (sq)))).
proof: Proof. apply/eqP; rewrite -(can2_eq (castmxKV _ _) (castmxK _ _)); apply/eqP. apply/rowP=> [] i; rewrite !(mxE, castmxE, esymK, cast_ord_id) /=. symmetry; case: splitP=> j hj /=; rewrite !mxE hj. case hst: sg_tab (sg_tab_nil (size sq))=> [|l 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 /constraints big_filter big_mkcond !sumMz; apply: congr_big=> // x _. rewrite nth_cat size_map ![size (_::_)]/= sst ltn_ord. rewrite (nth_map [::]) /= ?sst ?ltn_ord // big_ord_recl /=. by rewrite sgr_cp0 sgz_cp0; case: (_ < _); first by rewrite mul1n. case: splitP=> k hk; rewrite !mxE /= hk. case hst: sg_tab (sg_tab_nil (size sq))=> [|l 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 /constraints big_filter big_mkcond !sumMz; apply: congr_big=> // x _. rewrite nth_cat nth_cat !size_map ![size (_ :: _)]/= sst ltnNge leq_addr. rewrite (@nth_map _ [::] _ _ [eta cons (-1)] _ (l::st)) /= ?sst addKn ltn_ord //. rewrite big_ord_recl /= sgr_cp0 sgz_cp0. by case: (_ < _); first by rewrite mul1n. case hst: sg_tab (sg_tab_nil (size sq))=> [|l 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 /constraints big_filter big_mkcond !sumMz; apply: congr_big=> // x _. rewrite nth_cat nth_cat nth_cat !size_map ![size (_ :: _)]/= sst. rewrite (@nth_map _ [::] _ _ [eta cons 0] _ (l::st)) /=; last first. by rewrite !addKn sst ltn_ord. rewrite ltnNge leq_addr /= !addKn ltnNge leq_addr /= ltn_ord. rewrite big_ord_recl /= sgr_cp0 sgz_cp0. by case: (_ == _); first by rewrite mul1n. 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)