proposition: Lemma Exercise6_33k n u v: inc n c -> inc u (rho n) -> inc v (rho n) -> (u <=o v <-> gle E6_33_r (Vf (y n) u) (Vf (y n) v)).
proof: Proof. move => nc us vs. have or: ordinalp (rho n). exact: (proj32_1 (proj32 (Exercise6_33i nc))). move: (Exercise6_33j nc) =>[[qa qb qc qd] st ty]. have usy: inc u (source (y n)) by ue. have vsy: inc v (source (y n)) by ue. move: (qd u v usy vsy) => H. split => la. have: gle (ordinal_o (rho n)) u v. by apply/(ordo_leP (rho n) u v); split => //; case:la. by move/H; move/iorder_gle1. have fy: function (y n) by move: (proj31 qc) => bjy; fct_tac. have:gle (induced_order E6_33_r (Vf X n)) (Vf (y n) u) (Vf (y n) v). apply/iorder_gleP; split => //; Wtac. move:(Os_ordinal or us) (Os_ordinal or vs) => ou ov. by move/H /ordo_leP/proj33 => suv. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)