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