proposition: Lemma mat_build_nth : forall m n gen i j (ip : i < m) (jp : j < n), Vnth (Vnth (mat_build gen) ip) jp = gen i j ip jp.
proof: Proof. intros. fold (get_row (mat_build gen) ip). fold (get_elem (mat_build gen) ip jp). apply mat_build_elem. Qed.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)