fact: Definition ON_fun_ok {alpha: Ord} `{OA : @ON A ltA compareA} `{OB : @ON B ltB compareB} {iota : A -> Ord} {_ : ON_correct alpha OA iota} (f : A -> A) (g : Ord -> Ord) := forall x, iota (f x) = g (iota x).
imports: Coq(RelationClasses Relation_Operators Ensembles) hydras(OrdNotations Schutte_basics)