proposition: Lemma geq_add_remove : forall y s g g', ~In y g -> geq (add y s g) g' -> geq g (if XSet.is_empty s then g' else remove y g').
proof: Proof. intros y s g g' n e. case_eq (XSet.is_empty s); intros. rewrite geq_succs; intro z. rewrite <- e. rewrite succs_add. destruct (eq_dec y z). 2: refl. rewrite <- e0. unfold succs. rewrite not_find_in_iff in n. rewrite n. sym. apply is_empty_eq. hyp. rewrite geq_succs; intro z. unfold succs at 2. rewrite remove_o. case_eq (eq_dec y z); intros. rewrite <- e0. unfold succs. rewrite not_find_in_iff in n. rewrite n. refl. fold (succs z g'). trans (succs z (add y s g)). rewrite succs_add. rewrite H0. refl. rewrite e. refl. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)