fact: Definition mint_gt n (l r : mint n) := mint_ge l r /\ vec_at0 (const l) > vec_at0 (const r).
imports: Coq(Setoid) CoLoR(LogicUtil Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil AWFMInterpretation NatUtil AMatrixBasedInt)