proposition: Lemma sup_gt (S : set R) (x : R) : S !=set0 -> (x < sup S -> exists2 y, S y & x < y)%R.
proof: Proof. move=> S0; rewrite not_exists2P => + g; apply/negP; rewrite -leNgt. by apply sup_le_ub => // y Sy; move: (g y) => -[// | /negP]; rewrite leNgt. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid