proposition: Lemma iota_unique : forall (P : V -> Prop) (x : V), (forall y, P y -> y = x) -> P x -> iota P = x.
proof: Proof. intros P x HP Px. apply eq_close. intros eps. apply: iota_correct_weak Px eps. intros x' y Px' Py eps. rewrite (HP _ Py) -(HP _ Px'). apply ball_center. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub