fact: Definition mint_ge n (l r : mint n) := Vforall2 mat_ge (args l) (args r) /\ Vforall2 ge (AMatrixBasedInt.const l) (AMatrixBasedInt.const r).
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)