fact: Record ordered_subset (S: A → Prop) (R: relation A) := { S_proper:> Proper (eqA ==> iff) S; R_strict:> StrictOrder R; R_wellfounded: well_founded R; R_proper:> Proper (eqA ==> eqA ==> iff) R; R_carrier_correct: ∀ x y, R x y → S x ∧ S y; R_carrier_complete: ∀ x y, S x → S y → eqA x y ∨ R x y ∨ R y x }.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)