fact: Definition mat_eqA m n (M N : matrix m n) := forall i j (ip : i < m) (jp : j < n), get_elem M ip jp =A= get_elem N ip jp.
imports: Coq(List Setoid Morphisms) CoLoR(VecArith OrdSemiRing VecUtil NatUtil LogicUtil RelUtil)