proposition: Lemma Exercise6_33j n (r := induced_order E6_33_r (Vf X n)): inc n c -> [/\ order_isomorphism (y n) (ordinal_o (rho n)) r, source (y n) = rho n & target (y n) = (Vf X n)].
proof: Proof. move=> nc. have pa: order_isomorphism (y n) (ordinal_o (rho n)) r. by apply: the_ordinal_iso1; move: (Exercise6_33i nc) => []. move: (pa) => [_ _ [_ -> ->] _]. move: (Exercise6_33h) => [[pe pf] _ _]. by rewrite ordinal_o_sr /r (iorder_sr (proj1 pe)) // pf;apply: Exercise6_33e. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)