proposition: Lemma transitive_set_fold_trans_add_edge : forall x g, Transitive g -> forall s, Transitive (XSet.fold (trans_add_edge x) s g).
proof: Proof. intros x g gtrans s. pattern (XSet.fold (trans_add_edge x) s g). apply XSetProps.fold_rec_weak; split_all. apply transitive_trans_add_edge. hyp. Qed.
imports: Coq(OrderedType) CoLoR(RelUtil LogicUtil BoolUtil FGraph)