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