proposition: Lemma vec_to_col_mat_spec : forall n (v : vec n) i (ip : i < n) j (jp : j < 1), get_elem (vec_to_col_mat v) ip jp = Vnth v ip.
proof: Proof. intros. unfold get_elem. rewrite get_elem_swap. destruct j. rewrite get_col_col_mat. trivial. lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)