proposition: Lemma Exercise6_33a: infinite_c (a ^c b).
proof: Proof. have bnz := nesym (proj2(clt_leT clt_01 hb)). case iab => iiab; [apply: (CIS_pow iiab bnz) | apply:(CIS_pow3 ha iiab) ]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)