proposition: Lemma card_dominant_pr9 A B C: infinite_c B -> C <c A -> A <=c C ^c B -> A ^c B = C ^c B.
proof: Proof. move => ib ca le1. case: (equal_or_not C \0c) => cnz. move: le1; rewrite cnz (cpow0x (infinite_nz ib)) => az. case: (clt0 (clt_leT ca az)). have anz: A <> \0c. move=> h; rewrite h in ca; case: (clt0 ca). move: (cpow_Mleeq B le1 anz). rewrite - cpow_pow (csquare_inf ib) -/B => le4. exact: (cleA le4 (cpow_Mleeq B (proj1 ca) cnz)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)