proposition: Lemma int_lbound_has_minimum (B : set int) i : B !=set0 -> lbound B i -> exists j, B j /\ forall k, B k -> j <= k.
proof: Proof. move=> [i0 Bi0] lbBi; have [n i0in] : exists n, i0 - i = n%:Z. by exists `|i0 - i|%N; rewrite gez0_abs // subr_ge0; exact: lbBi. elim: n i lbBi i0in => [i lbBi /eqP|n ih i lbBi i0in1]. by rewrite subr_eq0 => /eqP i0i; exists i0; split =>// k Bk; rewrite i0i lbBi. have i0i1n : i0 - (i + 1) = n by rewrite opprD addrA i0in1 -addn1 PoszD addrK. have [?|/not_forallP] := pselect (lbound B (i + 1)); first exact: (ih (i + 1)). move=> /contrapT[x /not_implyP[Bx i1x]]; exists x; split => // k Bk. rewrite (le_trans _ (lbBi _ Bk)) //. by move/negP : i1x; rewrite -ltNge ltzD1. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra) mathcomp(mathcomp_extra boolp classical_sets set_interval) Setoid