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