proposition: Lemma vec_to_row_mat_idem : forall n (M : row_mat n), vec_to_row_mat (row_mat_to_vec M) = M.
proof: Proof. intros. apply mat_eq. intros. mat_get_simpl. destruct i. simpl. rewrite (lt_unique access_0 ip). refl. lia. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)