proposition: Lemma rel_trans_add_edge_list : forall g a, Transitive g -> trans_add_edge_list g a == add_edge_list g a!.
proof: Proof. intros g a tg. unfold trans_add_edge_list, add_edge_list. destruct (f a). 2: sym; apply trans_tc; hyp. destruct p as [x l]. revert g tg. induction l; simpl; intros g tg. sym. apply trans_tc. hyp. rename a0 into y. rewrite IHl. 2: apply transitive_trans_add_edge; hyp. unfold add_edge' at 3, trans_add_edge'. rewrite !rel_list_fold_left_add_edge, rel_add_edge, rel_trans_add_edge_prod. case_eq (XSet.mem y (succs x g)); intros. rewrite mem_succs_id. 2: hyp. refl. apply tc_eq. apply R.union_incl. refl. rewrite union_commut. apply R.union_incl. 2: refl. intros u v [xu yv]. unfold prod. rewrite xu, yv, !add_iff. intuition. rewrite union_incl_eq. split. apply incl_tc. apply incl_union_l. refl. rewrite union_incl_eq. split. rewrite prod_add_incl_tc_id. apply tc_incl. apply incl_union_r. refl. apply incl_tc. apply incl_union_r. apply incl_union_l. refl. Qed.
imports: Coq(OrderedType) CoLoR(RelUtil LogicUtil BoolUtil FGraph)