proposition: Lemma succeq_dec : rel_dec succeq.
proof: Proof. intros x y. unfold succeq. apply Vforall2_dec. intros m n. apply ge_dec. Defined.
imports: CoLoR(Matrix AMonAlg VecUtil OrdSemiRing ATrs LogicUtil RelUtil NatUtil AWFMInterpretation) Coq(PeanoNat Setoid Morphisms)