proposition: Lemma eq_vec_refl dim : forall (v:vector dim), eq_vec v v.
proof: Proof. induction v as [a | dim a v] using vector_ind. reflexivity. split;auto. reflexivity. Qed.
imports: Coq(Lia List Setoid Peano_dec Eqdep_dec Ring Zwf Morphisms ZArith) CoLoR(interp)