proposition: Lemma Exercise4_11b x: sub x A -> pure R x -> exists2 y, sub x y & max_pure A R y.
proof: Proof. move => xa px. set po:= (sub_order (set_of_pure A R)). move: (sub_osr (set_of_pure A R)) => [or sr]. have xsr: inc x (substrate po). by rewrite sr; apply: Zo_i => //; apply /setP_P. move: (inductive_max_greater or Exercise4_11a xsr). move => [m]; rewrite /po/maximal sr. move => [mp xm] /sub_gleP [_ _ sm]; move: mp => /set_of_pureP. move=> [ma prm]; exists m => //; split => // p pp cmp pa; symmetry; apply: xm. by apply /sub_gleP;split => //; apply: Zo_i => //; apply /setP_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)