proposition: Lemma get_col_col_mat : forall n (v : vec n) (p : 0 < 1), get_col (vec_to_col_mat v) p = v.
proof: Proof. induction v; intros. trivial. simpl. rewrite IHv. trivial. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)