Update reals/reals.v

Co-authored-by: Quentin VERMANDE <[email protected]>

Author: affeldt-aist

reals/reals.v

@@ -661,7 +661,7 @@ Lemma nat_has_minimum (A : set nat) : A !=set0 ->
 Proof.
 move=> A0.
 pose B : set int := [set x%:~R | x in A].
-have B0 : B !=set0 by case: A0 => a Aa; exists a%:~R, a.
+have B0 : B !=set0 by apply: image_nonempty.
 have : lbound B 0 by move=> _ [b0 Bb0 <-]; rewrite ler0z.
 move/(int_lbound_has_minimum B0) => [_ [[i Ai <-]]] Bi.
 exists i; split => // k Bk.