proposition: Lemma rel_list_fold_left_trans_add_edge_list : forall l g, Transitive g -> fold_left trans_add_edge_list l g == fold_left add_edge_list l g!.
proof: Proof. induction l; simpl. intros. sym. apply trans_tc. hyp. intros g tg. rewrite IHl. 2: apply transitive_trans_add_edge_list; hyp. rewrite rel_list_fold_left_add_edge_list. rewrite rel_list_fold_left_add_edge_list with (g:=add_edge_list g a). set (g0 := fold_left add_edge_list l empty). rewrite rel_trans_add_edge_list. 2: hyp. apply tc_eq. apply R.union_incl. refl. apply incl_tc. refl. rewrite union_incl_eq. split. apply incl_tc. apply incl_union_l. refl. apply tc_incl. apply incl_union_r. refl. Qed.
imports: Coq(OrderedType) CoLoR(RelUtil LogicUtil BoolUtil FGraph)