proposition: Lemma worder_adjoin_greatest r a: worder r -> ~ (inc a (substrate r)) -> worder (order_with_greatest r a).
proof: Proof. move=> wor nas. have [[on sn] rd [ _ gna]]:= (order_with_greatest_pr (proj1 wor) nas). apply:(worder_prop_rev on) => x xs nex. set (y := x \cap (substrate r)). case: (emptyset_dichot y) => ye. have xa: x = singleton a. apply: set1_pr1 => //. move=> z zx; move: (xs _ zx); rewrite sn; case /setU1_P => // zr. by empty_tac1 z; apply:setI2_i. have ax: inc a x by rewrite xa; fprops. by ex_tac; rewrite xa => t /set1_P ->; order_tac; apply: xs. have sys:sub y (substrate r) by apply: subsetI2r. move: (worder_prop wor sys ye)=> [z zy lez]. have zx:= (setI2_1 zy). exists z => // t tx. move: (xs _ tx); rewrite sn; case /setU1_P => p. have ty: inc t y by apply: setI2_i. by move: (lez _ ty) => pa; apply:setU2_1. by rewrite p; apply: gna; apply: xs. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)