proposition: Lemma succeq'_sub : succeq' << IR I succeq.
proof: Proof. intros t u tu. unfold I, succ. set (r := mkRule t u). change t with (lhs r). change u with (rhs r). apply pi_compat_rule_weak. hyp. Qed.
imports: CoLoR(APolyInt AMonAlg ZUtil RelUtil PositivePolynom ATrs MonotonePolynom LogicUtil BoolUtil)