fact: Definition pref_union X (r r' : relation X) x y := r x y \/ r' x y /\ ~ r y x.
imports: Arith micromega.Lia HahnBase HahnList HahnRelationsBasic HahnEquational HahnMaxElt HahnRewrite HahnDom HahnMinPath HahnPath