fact: Definition segment x (Cx : cond x) y (Cy : cond y) := filterP (fun e => ~ In e (starting_segment Cx)) (starting_segment Cy).
imports: HahnBase HahnSets HahnList HahnRelationsBasic HahnWf HahnMinElt HahnEquational HahnSorted