proposition: Lemma succ_succeq_compat : absorbs_left succ succeq.
proof: Proof. unfold absorbs_left, succ, succeq. intros t v [u [h1 h2]]. unfold proj_ord in *. apply succ_succeq_compat. exists (proj pi u). auto. Qed.
imports: CoLoR(ATrs LogicUtil ARelation RelUtil SN ListUtil AMannaNess ACompat BoolUtil BoundNat) CoLoR(AMonAlg) CoLoR(AFilterBool VecUtil) CoLoR(AFilterPerm) CoLoR(AProj)