proposition: Lemma add_pred_transp_geq : forall x s, transpose_neqkey geq (add_pred x s).
proof: Proof. unfold transpose_neqkey. intros x s w w' sw sw' g nww'. unfold geq, add_pred. destruct (XSet.mem x sw); destruct (XSet.mem x sw'); repeat rewrite rel_set_fold_add_edge; try refl. rewrite <- !R.union_assoc. apply R.union_same. apply union_commut. refl. Qed.
imports: Coq(OrderedType) CoLoR(RelUtil LogicUtil BoolUtil FGraph)