proposition: Lemma Exercise6_33a6 (bb := cnext b) : [/\ ordinalp bb, bb <c c, forall t, ordinalp t -> (t <o bb <-> cardinal t <=c b) & forall t, inc t bb -> ordinalp t /\ cardinal t <=c b ].
proof: Proof. move: (cnext_pr1 (proj32 hb)) =>[qa qb qc]. have obb: ordinalp bb by case: qa. have bbc: bb <c c by apply/Exercise6_33aP; apply/ qc; exact: Exercise6_33a3. have aux t: ordinalp t -> t <o bb <-> cardinal t <=c b. move => ot; move: (ocle2P qa ot) => h; split => //. by move/h => hh; apply: (cnext_pr4 (proj32 hb)). by move => hh; apply/h; apply: (cle_ltT hh qb). split => // t /(oltP obb) tlb; move: (proj31_1 tlb) => ot. by split => //;apply/ (aux t ot). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)