proposition: Lemma geq_succs : forall g g', geq g g' <-> forall x, succs x g [=] succs x g'.
proof: Proof. intros g g'. rewrite gle_antisym. rewrite !gle_succs. fo. Qed.
imports: Coq(OrderedType) CoLoR(ListUtil FSetUtil FMapUtil RelUtil LogicUtil)