proposition: Lemma transitive_list_fold_left_trans_add_edge : forall x l g, Transitive g -> Transitive (fold_left (trans_add_edge' x) l g).
proof: Proof. intro x. induction l; simpl. auto. intros g tg. apply IHl. apply transitive_trans_add_edge. hyp. Qed.
imports: Coq(OrderedType) CoLoR(RelUtil LogicUtil BoolUtil FGraph)