proposition: Lemma Vnth_col_mat : forall n (m : col_mat n) i (ip : i < n), Vnth (col_mat_to_vec m) ip = get_elem m ip access_0.
proof: Proof. induction m; intros. lia. destruct i. trivial. simpl. rewrite IHm. trivial. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)