proposition: Lemma geq_add : forall y s g g', ~In y g -> geq (add y s g) g' -> if XSet.is_empty s then geq g' g else Add y (succs y g') (remove y g') 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. apply is_empty_eq. hyp. unfold Add. intro z. rewrite add_o. case_eq (eq_dec y z); intros. unfold succs. rewrite e0. case_eq (find z g'); intros. refl. rewrite geq_succs in e. ded (e y). rewrite succs_add_id in H2. rewrite e0 in H2. unfold succs in H2. rewrite H1 in H2. rewrite <- is_empty_eq in H2. rewrite H in H2. discr. rewrite remove_o. rewrite H0. refl. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)