proposition: Lemma order_with_greatest_pr r a (r':=order_with_greatest r a): order r -> ~ (inc a (substrate r)) -> [/\ order_on r' ((substrate r) +s1 a), r = induced_order r' (substrate r) & greatest r' a].
proof: Proof. rewrite /r' /order_with_greatest => or nas {r'}. set r':= union2 r _. have jaa: inc (J a a) (((substrate r) +s1 a) *s1 a) by apply:indexed_pi; fprops. have src:= (sub_graph_coarse_substrate (proj41 or)). have gr': sgraph r' by rewrite /r'/indexed; apply: setU2_graph; fprops. have sr': substrate r'= (substrate r) +s1 a. set_extens x. move =>t; apply/setU1_P. case /(substrate_P gr'):t => [][y] /setU2_P []; try (left; substr_tac); move/setXp_P => []; [by move/setU1_P | by move => _ /set1_P => h;right]. case /setU1_P => hh; apply: (@arg1_sr _ x x). by apply:setU2_1; order_tac. by rewrite hh; apply:setU2_2. have rr: reflexivep r'. move => y;rewrite sr';case /setU1_P. by move=> hyp;apply:setU2_1; order_tac. move=> ->;apply:setU2_2; fprops. have tr:transitivep r'. move=> x y z;case /setU2_P=> h; case /setU2_P=> h'. + apply:setU2_1; order_tac. + apply:setU2_2; apply/setXp_P; move/setXp_P: h' => [pa pb];split => //. apply:setU2_1; substr_tac. + move/setXp_P: h => [pa pb]; case: nas; move/set1_P: pb => <-; substr_tac. + move/setXp_P: h' => [_] /set1_P ->; move/setXp_P: h => [pb] _. by apply:setU2_2; apply: indexed_pi. have ar:antisymmetricp r'. move=> x y;case /setU2_P=> h; case /setU2_P=> h'. + order_tac. + case: nas; move/setXp_P: h' => [_] /set1_P <-; substr_tac. + case: nas; move/setXp_P: h => [_] /set1_P <-; substr_tac. + by move/setXp_P: h => [_] /set1_P ->; move/setXp_P: h' => [_] /set1_P ->. have or': order r' by []. split => //. rewrite /r' /induced_order; set_extens x => xr. by apply: setI2_i; [ apply/setU2_P; left| apply: src]. case/setI2_P: xr => /setU2_P [] //. by move /setX_P => [_ _] /set1_P qa /setX_P [_ _]; rewrite qa. hnf; rewrite sr'; split; fprops. by move=> x xe; apply /setU2_P; right; apply: indexed_pi. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)