proposition: Lemma partition_succeq_compat : forall R, snd (partition part_succeq R) = nil -> compat IR_succeq (snd (partition part_succ R)).
proof: Proof. clear R. intros R Rpart l r lr. apply succeq'_sub. apply partition_by_rel_true with MA.term succeq'_dec. apply rule_partition_left with R. fold part_succeq. ded (partition_complete part_succeq (mkRule l r) R). simpl in H. rewrite Rpart in H. destruct H. apply partition_inright with part_succ. hyp. hyp. destruct H. Qed.
imports: CoLoR(ATrs RelUtil SN ListUtil ARelation LogicUtil) CoLoR(ACompat)