proposition: Lemma Exercise_6_20c1 a: GenContHypothesis -> regular_cardinal a -> (forall m, \0c <c m -> m <c a -> a ^c m = a).
proof: Proof. move => gch /regular_cardinalP [ia ra] m [_ m0] ma. move: (infinite_power10 gch m ia); move=> [_ pa _ _]. by apply: pa; [ apply:nesym | ue]. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)