proposition: Lemma rel_trans_add_edge_prod : forall x y g, trans_add_edge x y g == if XSet.mem y (succs x g) then g else prod (XSet.add x (preds x g)) (XSet.add y (succs y g)) U g.
proof: Proof. intros x y g. rewrite rel_trans_add_edge_pred_succ. destruct (XSet.mem y (succs x g)). refl. cbv zeta. set (ysy := XSet.add y (succs y g)). set (xpx := XSet.add x (preds x g)). rewrite <- R.union_assoc. apply R.union_same. apply pred_succ_prod. refl. Qed.
imports: Coq(OrderedType) CoLoR(RelUtil LogicUtil BoolUtil FGraph)