proposition: Lemma Zorn_aux_eff r (m n: fterm): order r -> (forall s, sub s (substrate r) -> worder (induced_order r s) -> upper_bound r s (m s)) -> (forall x, inc x (substrate r) -> glt r x (n x)) -> False.
proof: Proof. move=> or mp np. set (E:= substrate r). set (s:= Zo (\Po E) (fun z => (worder (induced_order r z)))). have sp: sub s (\Po E) by rewrite /s; apply: Zo_S. pose p s := n (m s). have mp1 x: inc x s -> upper_bound r x (m x). by move => /Zo_P [/setP_P sa sb]; apply: mp. have Ha x: inc x s -> inc (p x) E. move/mp1 => [/np lt _]; rewrite/E; order_tac. have Hb x: inc x s -> upper_bound r x (p x). move/mp1 =>[qa qb]; move:(np _ qa) => [qc _]. split; [ order_tac |]; move => y /qb => lr; order_tac. have Hc x: inc x s -> ~ inc (p x) x. move => xs pxx. move/mp1: (xs) =>[qa qb]; move:(np _ qa) => [qc qd]. move:(qb _ pxx) => ba; case qd; order_tac. have zp x: inc x s -> inc (p x) (E -s x). move => zs; apply/setC_P; split; fprops. move: (Zermelo_aux sp zp); set r' := union _. move =>[[xor so ww] ns]. move: (iorder_osr or so) => [oi sr1]. have ext: sub r' (induced_order r (substrate r')). move=> x xr. move:(pr1_sr xr)(pr2_sr xr) => Ps Qs. have gr: sgraph r' by fprops. move: (gr _ xr) => xp; rewrite -xp; rewrite - xp in xr. case: (equal_or_not (P x) (Q x)) => aux. rewrite aux; order_tac; rewrite iorder_sr //. have ltPQ: glt r' (P x) (Q x) by split. have Pse: (inc (P x) (segment r' (Q x))) by apply/segmentP. apply /iorder_gle0P => //. move: (ww _ Qs) => [p1 <-]. by apply: (proj2 (Hb _ p1)). have r'v: r' = induced_order r (substrate r'). apply: extensionality => // t tio. have p1: order (induced_order r (substrate r')) by fprops. have p2: sgraph (induced_order r (substrate r')) by fprops. move: (p2 _ tio) => pt. move:(pr1_sr tio)(pr2_sr tio); rewrite sr1 => Ps Qs. rewrite -pt in tio *. case: (total_order_pr2 (worder_total xor) Qs Ps) =>//. move=> [lePQ nPQ]; move: (ext _ lePQ)=>tio'; case: nPQ; order_tac. rewrite r'v in xor. by case ns; apply:Zo_i;first apply/setP_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)