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