proposition: Lemma cvec_tvec z sq : zmxR (cvec z (sq)) = (zmxR (tvec z (sq))) *m (invmx (zmxR (ctmat (size (sq))))).
proof: Proof. apply/eqP; set A := zmxR (ctmat _). rewrite -(@can2_eq _ _ (fun (x : 'rV_(_)) => x *m A) (fun x => x *m (invmx A))). * by rewrite /A -map_mxM ?tvec_cvec//; apply: zinjR_morph. * by apply: mulmxK; rewrite /A ctmat_unit. * by apply: mulmxKV; rewrite /A ctmat_unit. 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)