proposition: Lemma term_ge_dec : rel_dec term_ge.
proof: Proof. intros l r. unfold term_ge, term_ord. simpl. match goal with |- {mint_ge ?l ?r} + {~mint_ge ?l ?r} => destruct (mint_ge_dec l r); auto end. Defined.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)