proposition: Lemma rel_trans_add_edge : forall x y g, Transitive g -> trans_add_edge x y g == add_edge x y g!.
proof: Proof. intros x y g tg. cut (Transitive (trans_add_edge x y g)). 2: apply transitive_trans_add_edge; hyp. rewrite rel_add_edge. rewrite !rel_trans_add_edge_prod. case_eq (XSet.mem y (succs x g)); intros. rewrite mem_succs_id. rewrite trans_tc. refl. hyp. hyp. split. rewrite union_incl_eq. split. apply prod_add_incl_tc_id. trans (g U id x y). apply incl_union_l. refl. apply incl_tc. refl. apply tc_min. 2: hyp. rewrite union_commut. apply R.union_incl. 2: refl. intros a b [xa yb]. split; rewrite add_iff; intuition. Qed.
imports: Coq(OrderedType) CoLoR(RelUtil LogicUtil BoolUtil FGraph)