proposition: Lemma succs_trans_add_edge_id : forall x y g, succs x (trans_add_edge x y g) [=] if XSet.mem y (succs x g) then succs x g else XSet.union (XSet.add y (succs y g)) (succs x g).
proof: Proof. intros x y g. unfold trans_add_edge. case_eq (XSet.mem y (succs x g)); intros. refl. intro z. rewrite In_succs_rel, rel_map_fold_add_pred_ext, rel_set_fold_add_edge_ext. unfold pred, succ. rewrite union_iff. rewrite !add_iff, !In_succs_rel. split_all; auto with ordered_type. Qed.
imports: Coq(OrderedType) CoLoR(RelUtil LogicUtil BoolUtil FGraph)