proposition: Lemma pred_succ_prod : forall x y g, let ysy := XSet.add y (succs y g) in let xpx := XSet.add x (preds x g) in pred x ysy g U succ x ysy == prod xpx ysy.
proof: Proof. intros x y g. cbv zeta. set (ysy := XSet.add y (succs y g)). set (xpx := XSet.add x (preds x g)). split. rewrite union_incl_eq. split; intros a b [h1 h2]; split. unfold xpx. rewrite add_iff. right. rewrite In_preds_rel. hyp. hyp. unfold xpx. rewrite add_iff. left. hyp. hyp. intros a b [h1 h2]. unfold Relation_Operators.union, pred, succ. subst xpx ysy. rewrite add_iff in h1, h2. rewrite !add_iff. rewrite In_preds_rel in h1. rewrite In_succs_rel in h2. rewrite !In_succs_rel, (eq_com a x). tauto. Qed.
imports: Coq(OrderedType) CoLoR(RelUtil LogicUtil BoolUtil FGraph)