proposition: Lemma ex5_Mij_pr1 i j x (M:= ex5_M i j x): gle (psr S) i j -> inc x (Vg Gf i) -> inc M (ex5_X i j x) /\ forall t, inc t (ex5_X i j x) -> gle (Vg Er j) t M.
proof: Proof. move => ha hb. move:(prl_prop0 ha) => [iI jI]. move:(proj1 (lEr jI))(sEr jI) => or sr. move:(ex5_Xij_pr2 ha (x:=x)); rewrite - sr => ss. move: (iorder_osr or ss) => [or' sr']. case:(the_greatest_pr or' (ex5_G7 ha hb)); rewrite iorder_sr //. by move => ra rb; split => //; move => t/rb /iorder_gle1. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)