proposition: Lemma Zermelo_v1 E (p:= fun x => rep (E -s x)) (s:=(\Po E) -s1 E) (r := union (Zo (\Po coarse E) (Zermelo_ax E p s))): worder_on r E.
proof: Proof. have p1: sub s (\Po E) by rewrite /s; apply: sub_setC. have p2: forall x, inc x s -> inc (p x) (E -s x). move=> x xs; rewrite /p; apply: rep_i. apply: setC_ne. by move: xs => /setC_P [] /setP_P pa /set1_P xe. have p3: forall x, inc x s -> (inc (p x) (E -s x)). by move => x xs; move: (p2 _ xs). move: (Zermelo_aux p1 p3) => [[xor so _] ns]. split => //;ex_middle h; case: ns. by apply/setC_P; split; [ apply /setP_P | move/set1_P]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)