proposition: Lemma completeness_any : forall P : R -> Prop, ( forall x y, x <= y -> P y -> P x ) -> forall He : (exists x, P x), forall Hb : (bound P), forall x, x < proj1_sig (completeness _ Hb He) -> ~ ~ P x.
proof: Proof. intros P HP He Hb x. case completeness => y [Hy1 Hy2] /= Hxy Px. apply Rle_not_lt with (2 := Hxy). apply Hy2 => t Pt. apply Rnot_lt_le => Hxt. apply Px. apply: HP Pt. now apply Rlt_le. Qed.
imports: Coq(Reals List ssreflect) Rcomplements