proposition: Lemma row_mat_to_vec_idem : forall n (v : vec n), row_mat_to_vec (vec_to_row_mat v) = v.
proof: Proof. intros. apply Veq_nth. intros. mat_get_simpl. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)