fact: Record well_order {A} (eqA ltA: relation A) := { eqA_equiv :> Equivalence eqA; ltA_strict :> StrictOrder ltA; ltA_wellfounded: well_founded ltA; ltA_proper :> Proper (eqA ==> eqA ==> iff) ltA; ltA_total: ∀ x y, eqA x y ∨ ltA x y ∨ ltA y x }.
imports: Coq(Relations Equivalence Morphisms Utf8) Coq(ChoiceFacts ClassicalFacts) Coq.Program(Basics) Coq.Logic(SetoidChoice)