proposition: Lemma Vnth_row_mat : forall n (m : row_mat n) i (ip : i < n), Vnth (row_mat_to_vec m) ip = get_elem m access_0 ip.
proof: Proof. trivial. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)