fact: Definition pred_compatible A (E:A->A->Prop) (Q:A->Prop) := forall x y, Q x -> E y x -> Q y.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)