fact: Fixpoint matrix (n:nat) {struct n} : Type := match n with | 0%nat => A | S n => (A*((vector n)*((vector n) * (matrix n))))%type end.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)