fact: Definition suspend (o: order) x (x_not_in: ¬o.S x): order := exist _ (suspend_S (o.S) x, suspend_R (o.S) (o.R) x) (suspend_good (o.S) (o.R) x x_not_in (o.good)).
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)