proposition: Theorem adjoin_greatest r a E: order_on r E -> ~ (inc a E) -> exists !r', [/\ order_on r' (E +s1 a), r = induced_order r' E & greatest r' a].
proof: Proof. move=> [or sr] naE. set (E':=E +s1 a). set (r':=r \cup (E' \times (singleton a))). apply /unique_existence; split. exists (order_with_greatest r a). rewrite - sr in naE; move: (order_with_greatest_pr or naE); ue. pose p x := [/\ order_on x E', r = x \cap (coarse E) & greatest x a]. suff : forall x y, p x -> p y -> sub x y. move=> hyp x y px py. apply: extensionality; [ apply: hyp px py | apply: hyp py px]. move=> x y [[ox sx] ix gx] [[oy sy] iy gy] z zx. have pz:=(proj41 ox _ zx). move: (pr1_sr zx)(pr2_sr zx); rewrite sx => PzE QzE. case/setU1_P: PzE=> Pz. case /setU1_P: QzE=> Qz. have: (inc z r) by rewrite ix;apply: setI2_i=> //; apply /setX_P. by rewrite iy; move /setI2_P => []. move: gy=>[ay ga];rewrite -pz Qz; apply: ga; rewrite sy /E'; fprops. case /setU1_P: QzE => Qz. have rel2 : gle x (Q z) (P z). move: gx=>[ax ga]; rewrite Pz; apply: ga; rewrite sx /E'; fprops. move: zx; rewrite -{1} pz. rewrite -/(related _ _ _) -/(gle _ _ _)=> rel1. have PQ: P z = Q z by order_tac. by case: naE; rewrite -Pz PQ. rewrite -pz Qz; move: gy=>[ax]; apply; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)