proposition: Lemma succ_dec : rel_dec succ.
proof: Proof. apply intersection_dec. apply succeq_dec. intros x y. apply gt_dec. Defined.
imports: Coq(Setoid) CoLoR(LogicUtil Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil AWFMInterpretation NatUtil AMatrixBasedInt)