proposition: Lemma mint_ge_dec : forall n, rel_dec (@mint_ge n).
proof: Proof. intros n x y. unfold mint_ge. destruct (Vforall2_dec (@mat_ge_dec dim dim) (args x) (args y)); destruct (Vforall2_dec ge_dec (AMatrixBasedInt.const x) (AMatrixBasedInt.const y)); split_all; right; tauto. Defined.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)