proposition: Lemma cpow_pr a b a' b': a =c a' -> b =c b' -> a ^c b = a' ^c b'.
proof: Proof. move=> /card_eqP[f [bf sf tf]] /esym /card_eqP[g [bg sg tg]]; apply /card_eqP. exists (compose3function g f); hnf. rewrite {2 3} /compose3function - sf -tf - sg -tg; aw. by split => //;apply: c3f_fb. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)