proposition: Lemma the_nondominant_least_pr1 A B (C:= the_nondominant_least A B): ~ (rel_strong_card A B) -> cardinalp A -> [/\ C <c A, A <=c C ^c B & (forall t, t <c A -> A <=c t ^c B -> C <=c t)].
proof: Proof. move => h cA. rewrite /C/the_nondominant_least. apply select_pr; last first. move => x y p1 [p2 p3 p4] q1 [q2 q3 q4]. exact: (cleA (p4 _ q2 q3) (q4 _ p2 p3)). pose p c := c <c A /\ A <=c c ^c B. have [c cp]: exists c, p c. ex_middle h1; case: h. move => u ua. have cp: cardinalp (u ^c B) by fprops. case: (cleT_el (proj32_1 ua) cp) => // h2. case: h1; exists u; rewrite /p;split => //. have oc: ordinalp c by move: cp => [[[[cx _] _] _] _]. move: (least_ordinal4 oc cp);set z := least_ordinal _ _. move=> [_ [p1 p2] p3]. have iaa: inc z A. by move: (oclt p1) => /oltP0 [_ _]. ex_tac;split => // => t ta le. have pt: (p t) by split. have ot: ordinalp t by move: pt => [[[[cx _] _] _] _]. move: (ocle1 (p3 _ ot pt)). rewrite (card_card (proj31_1 p1)). by rewrite (card_card (proj31_1 (proj1 pt))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)