proposition: Lemma Exercise6_33i n: inc n c -> [/\ worder (induced_order E6_33_r (Vf X n)), \0o <o rho n & inc (rho n) (cnext b) ].
proof: Proof. move => ni; rewrite /E6_33_rho. set r := induced_order _ _. move: Exercise6_33h => [[wo1 sr] oi oie]. move: (Exercise6_33e ni); rewrite - sr => pa. have wor: worder r by move: (induced_wor wo1 pa). move: Exercise6_33d => [[fx ix] ss tx]; rewrite - ss in ni. move: (Vf_target fx ni); rewrite tx => /setC1_P [/HF2 hc hd]. have he: ordinal r <> \0o. move => h2; move:(ordinal0_pr2 wor h2); rewrite /r iorder_sr;fprops. have or: ordinalp (ordinal r) by apply OS_ordinal. have op: \0c <o (ordinal r) by apply: ord_ne0_pos. have aux: cardinal (ordinal r) <=c b. by rewrite (cardinal_of_ordinal wor) (iorder_sr (proj1 wo1) pa). by move/(proj43 (Exercise6_33a6) _ or): aux => /olt_i h. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)