proposition: Lemma infinite_power1_a a b: \2c <=c a -> a <=c b -> infinite_c b -> a ^c b = \2c ^c b.
proof: Proof. move => pa pb pc; apply: infinite_power1 => //. exact: (cleT pb (proj1 (cantor (proj1 pc)))). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)