proposition: Lemma add_edge_incl_trans : forall x y g, add_edge x y g << trans_add_edge x y g.
proof: Proof. intros x y g. rewrite rel_add_edge, rel_trans_add_edge_pred_succ. case_eq (XSet.mem y (succs x g)); intros. rewrite mem_succs_id. refl. hyp. cbv zeta; set (ysy:=XSet.add y (succs y g)). rewrite <- R.union_assoc, union_incl_eq. split. apply incl_union_r. refl. apply incl_union_l. apply incl_union_r. unfold ysy. rewrite succ_add. apply incl_union_l. refl. Qed.
imports: Coq(OrderedType) CoLoR(RelUtil LogicUtil BoolUtil FGraph)