proposition: Lemma transitive_trans_add_edge : forall x y g, Transitive g -> Transitive (trans_add_edge x y g).
proof: Proof. intros x y g tg. rewrite rel_trans_add_edge_prod. destruct (XSet.mem y (succs x g)). hyp. intros a b c. unfold Relation_Operators.union, prod. rewrite !add_iff. repeat rewrite In_preds_rel, In_succs_rel. split_all. rewrite H0, H1. intuition. left. split_all. right. apply tg with b; hyp. rewrite H0. tauto. left. split_all. right. apply tg with b; hyp. rewrite H, H1. intuition. rewrite H1. tauto. left. split_all. right. apply tg with b; hyp. left. split_all. right. apply tg with b; hyp. right. apply tg with b; hyp. Qed.
imports: Coq(OrderedType) CoLoR(RelUtil LogicUtil BoolUtil FGraph)