fact: Definition lesser_fixed_point A B (E:binary B) (F:(A->B)->(A->B)) := fun f g => (generally_consistent_partial_fixed_point E F f -> extends E f g) /\ (consistent E g f).
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)