proposition: Lemma optimal_fixed_point_unique : forall A B (E:binary B) (F:(A->B)->(A->B)), equiv E -> at_most_one_upto (partial_equiv E) (optimal_fixed_point E F).
proof: Proof. Proof using. introv Equi [Fix1 Ge1] [Fix2 Ge2]. applys~ order_wrt_antisym (extends_order A Equi). Qed.
imports: TLC(LibTactics LibLogic LibReflect LibEpsilon LibInt LibProd LibSum LibOperation LibRelation LibWf LibOrder LibMin)