proposition: Lemma Fix_prop_of_optimal: forall A B (E:binary B) (F:(A->B)->(A->B)) (f:A-->B), optimal_fixed_point E F f -> Fix_prop (partial_equiv E) (lesser_fixed_point E F) (partialize F) f.
proof: Proof. Proof using. introv [Gf Uf]. lets [Ff Cf]: Gf. split. rewrite~ partial_fixed_point_definitions in Ff. intros f' Ff'. split. intros Cf'. applys~ Uf. apply Gf. rewrite~ partial_fixed_point_definitions. Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)