fact: Definition inverse_matrix inv m n (M : matrix m n) : matrix m n := mat_build (fun i j ip jp => inv (get_elem M ip jp)).
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)