proposition: Lemma fo_inductive E: inductive (finer_order E).
proof: Proof. move=> X XsE tX. move:(fo_osr E) => [or sr]. case: (emptyset_dichot X) => xE. exists (diagonal E); split; last by rewrite xE => y /in_set0. rewrite sr;apply /ordersP; exact: (diagonal_osr E). have pa: forall x, inc x X -> (order_on x E). by move=> x xX; move: (XsE _ xX); rewrite sr => /ordersP. move: xE => [w wX]; move: (pa _ wX) => [sw ow]. exists (union X). set r:=finer_order E. have op: (forall a b, inc a (substrate r) -> inc b (substrate r) -> (gle r a b <-> sub a b)). move=> x y xsr ysr; split; first by move /fo_gleP => [_ _ _ _]. move => sa; apply /fo_gleP. by move: xsr ysr;rewrite sr => /ordersP[ra rb] /ordersP [rc rd]. have oq a b: inc a (substrate r) -> inc b (substrate r) -> gle r a b -> sub a b. by move => ha hb hc; apply/op. have ug: (sgraph (union X)). move=> y /setU_P [z yz zX];move: (pa _ zX) => [oz _]. by apply: (order_sgraph oz). have su: (substrate (union X) = E). set_extens t. move /(substrate_P ug); case; move=> [y] => /setU_P [z Jz zX]; move: (pa _ zX); move=> [oe <-]; substr_tac. move => te. have Jx: (inc (J t t) w) by order_tac; ue. have jy: inc (J t t) (union X) by union_tac. substr_tac. move: tX => [orX]; rewrite iorder_sr // => tX. suff usr: (inc (union X) (substrate r)). by move: (induced_sub_pr2 or op XsE usr) => /(lubP or XsE) []. rewrite /r sr; apply /ordersP;split => //. split => //. move => t; rewrite su => te; apply /setU_P; exists w => //; order_tac; ue. move => y x z /setU_P [a Ja aX] /setU_P [b Jb bX]. move: (pa _ aX) (pa _ bX) => [sa oa] [sb ob]. move: (XsE _ aX) (XsE _ bX) => asr bsr. case: (tX _ _ aX bX); move=> ab;move:(iorder_gle1 ab)=> cp. exact:(setU_i (proj43 sb _ _ _ (oq a b asr bsr cp _ Ja) Jb) bX). exact:(setU_i(proj43 sa _ _ _ Ja (oq b a bsr asr cp _ Jb)) aX). move => x y /setU_P [a Ja aX] /setU_P [b Jb bX]. move: (pa _ aX) (pa _ bX) => [sa oa] [sb ob]. have ia: inc a (substrate r) by apply: XsE. have ib: inc b (substrate r) by apply: XsE. case: (tX _ _ aX bX); move=> ab;move:(iorder_gle1 ab) => cp. move:(oq _ _ ia ib cp _ Ja)=> Jb'; order_tac. move:(oq _ _ ib ia cp _ Jb)=> Jb'; order_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)