fact: Definition Fix_prop A (E C:binary A) (F:A->A) (x:A) := max_element C (fixed_point E F) x.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)