proposition: Lemma ex4d_orderIr_prop1 A: infinite_set A -> ex4_prop_IR (ex4d_orderI A)(ex4d_orderr A).
proof: Proof. move => h. move: (finite_subsets_order A) => [qa qb qc qd qe]. move: (qa) => [pa pb]. split => //. - exists emptyset;apply/Zo_P; split; [ apply:setP_0i| apply: emptyset_finite]. - rewrite /greatest pb;move => x xI [_ xg]. have: ssub x A. move/Zo_P: xI => [/setP_P xA xf]; split => // exa. by case: (proj2 xf); rewrite exa. move/setC_ne=> [y /setC_P [yA]]; case. move: (xg _ (qb _ _ xI (qd _ yA))) => /sub_gleP [_ _]; apply; fprops. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)