proposition: Lemma constraints1_tvec : forall z sq, (constraints z (sq) (nseq (size (sq)) 1))%:~R = (castmx (erefl _, exp3n _) (zmxR (tvec z (sq)) *m (invmx (zmxR (ctmat (size (sq))))))) ord0 ord0.
proof: Proof. move=> z sq. rewrite -cvec_tvec castmxE /= cast_ord_id /= /cvec !mxE //= intz. congr ((constraints _ _ _)%:~R); elim: sq=> //= _ s -> /=. set l := sg_tab _; suff: size l != 0%N by case: l. exact: size_sg_tab_neq0. 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)