fact: Definition eq_mint k (mi1 mi2 : mint k) := let (c1, args1) := mi1 in let (c2, args2) := mi2 in c1 =v c2 /\ Vforall2 mat_eqA args1 args2.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)