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