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