proposition: Lemma preds_trans_add_edge_id : forall x y g, preds x (trans_add_edge x y g) [=] if XSet.mem y (succs x g) then preds x g else if XSet.mem x (XSet.add y (succs y g)) then XSet.add x (preds x g) else preds x g.
proof: Proof. intros x y g. unfold trans_add_edge. case_eq (XSet.mem y (succs x g)); intros. refl. set (ysy := XSet.add y (succs y g)). intro z. rewrite In_preds_rel, rel_map_fold_add_pred_ext, rel_set_fold_add_edge_ext. case_eq (XSet.mem x ysy); intros. rewrite add_iff, In_preds_rel. unfold ysy in H0. rewrite XSetFacts.add_b, orb_eq, eqb_ok, mem_succs_rel in H0. unfold ysy, pred, succ. rewrite add_iff, In_succs_rel. split_all; auto with ordered_type. unfold ysy, pred, succ. rewrite add_iff, In_succs_rel, In_preds_rel. rewrite false_not_true in H, H0. unfold ysy in H0. rewrite <- mem_iff, add_iff, In_succs_rel in H0. rewrite mem_succs_rel in H. split_all; contr. Qed.
imports: Coq(OrderedType) CoLoR(RelUtil LogicUtil BoolUtil FGraph)