proposition: Lemma mint_gt_dec : forall n, rel_dec (@mint_gt n).
proof: Proof. intro. apply intersection_dec. apply mint_ge_dec. intros x y. apply gt_dec. Defined.
imports: Coq(Setoid) CoLoR(LogicUtil Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil AWFMInterpretation NatUtil AMatrixBasedInt)