fact: Fixpoint create_vec (n:nat) (a:A) {struct n}: vector n := match n as u return vector u with | 0 => a | S n' => (a,@create_vec n' a) end.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)