proposition: Lemma iota_correct : forall P : V -> Prop, (exists! x : V, P x) -> P (iota P).
proof: Proof. intros P [x [Px HP]]. rewrite (iota_unique _ x) ; try exact Px. intros y Py. now apply sym_eq, HP. Qed.
imports: Coq(Reals Psatz ssreflect) Rcomplements Rbar Markov Iter Lub