proposition: Lemma vec_to_col_mat_idem : forall n (M : col_mat n), vec_to_col_mat (col_mat_to_vec M) = M.
proof: Proof. intros. apply mat_eq. intros. mat_get_simpl. destruct j. rewrite (lt_unique access_0 jp). refl. lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)