proposition: Lemma Exercise6_33l: M = unionf (cnext b) Mi.
proof: Proof. set_extens x; last by move /setUf_P => [t yp /Zo_S]. move: Exercise6_33d => [[fc ix] sx tx]. move => xM; move: (xM) => /setUb_P; aw; move => [t ts]; rewrite LgV// => xW. move: (Exercise6_33j ts) => [[o1 o2 [bf sf tf] _] sy ty]. rewrite - ty in xW. move: (proj2 (proj2 bf) _ xW) => [n ns xv]. move:(ordinal_transitive (proj41 (Exercise6_33a6)) (proj33(Exercise6_33i ts))). rewrite - sy => qa. by apply /setUf_P; exists n; [apply: qa | apply: (Zo_i xM); exists t]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)