proposition: Lemma ex5_Mij_pr2 i j x (M:= ex5_M i j x): gle (psr S) i j -> inc x (Vg Gf i) -> Vf (ex5_f i j) M = x /\ forall t, inc t (Vg (psE S) j) -> Vf (ex5_f i j) t = x -> gle (Vg Er j) t M.
proof: Proof. move => ha hb. move:(ex5_Mij_pr1 ha hb) => [/(ex5_Xij_pr x ha) [hc1 hc2] hd]. by split => // t ta tb; apply: hd; apply/(ex5_Xij_pr x ha t). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)