proposition: Lemma rel_trans_add_edge_pred_succ : forall x y g, trans_add_edge x y g == if XSet.mem y (succs x g) then g else let ysy := XSet.add y (succs y g) in pred x ysy g U (succ x ysy U g).
proof: Proof. intros x y g. unfold trans_add_edge. case_eq (XSet.mem y (succs x g)); intros. refl. rewrite rel_map_fold_add_pred. apply R.union_same. refl. rewrite rel_set_fold_add_edge. refl. Qed.
imports: Coq(OrderedType) CoLoR(RelUtil LogicUtil BoolUtil FGraph)