proposition: Lemma inductive_max_greater r a: order r -> inductive r -> inc a (substrate r) -> exists2 m, maximal r m & gle r a m.
proof: Proof. move=> or isr asr. set (F:= Zo (substrate r)(gle r a)). have Fs: sub F (substrate r) by rewrite /F; apply: Zo_S. move: (iorder_osr or Fs) => [oi sr]. have aF: inc a F by rewrite /F; apply: Zo_i=> //; order_tac. suff isF: inductive (induced_order r F). move:(Zorn_lemma oi isF)=> [b []]; rewrite iorder_sr // => bF bm. move: (bF) => /Zo_P [bs ab]. exists b => //; split =>// x h. apply: bm; apply/iorder_gle0P => //; apply: Zo_i; order_tac. move=> u; rewrite iorder_sr // => uF; rewrite iorder_trans // => toi. have tos: (sub (u +s1 a) (substrate r)). by apply: sub_trans Fs => t; case /setU1_P ; [ apply: uF| move=> ->]. move: (iorder_osr or tos) => [oit sit]. have toit: total_order (induced_order r (u +s1 a)). split=>//; rewrite sit. have susr: sub u (substrate r) by apply: sub_trans Fs. move=> x y; case /setU1_P=> hx; case /setU1_P => hy. - move: toi => [_]; rewrite iorder_sr // => h. move: (h _ _ hx hy); case => xx; [left | right]; apply/iorder_gle0P; fprops; apply (iorder_gle1 xx). - rewrite hy;right; apply/iorder_gle0P; fprops. by move: (uF _ hx); move /Zo_P => []. - rewrite hx;left; apply/iorder_gle0P; fprops. by move: (uF _ hy); move /Zo_P => []. - rewrite hx hy; left;apply/iorder_gle0P; fprops. by move: aF; move /Zo_P => []. move: (isr _ tos toit) => [b [bs bub]]. move: (bub _ (setU1_1 u a)) => ab. have bF: inc b F by rewrite /F; apply: Zo_i. exists b; split; first by rewrite iorder_sr //. move => y yu. by move: (bub _ (setU1_r a yu)) => yb; apply/iorder_gle0P => //; apply: uF. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)