proposition: Lemma min_exists (P: T1 -> Prop) x: ex_middle -> T1nf x -> (P x) -> exists y, T1nf y /\ P y /\ forall z, T1nf z -> P z -> y <= z.
proof: Proof. move => EM;move: x; apply: T1transfinite_induction. move => x nx H px. case (ex_middle_pick (fun z => (P z /\ ~ (x <= z))) EM). move => [z [pa [pb pc]]]. have zx: z < x by rewrite (T1ltNge z x); apply /negP. exact: (H _ pa zx pb). move => qf. exists x; split => //; split => // z pa pb; case xz: (x <= z) => //. by case (qf _ pa); rewrite xz. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)