proposition: Lemma cpow_pow a b c: a ^c (b *c c) = (a ^c b) ^c c.
proof: Proof. rewrite -csum_of_same cpow_sum - cprod_of_same. aw. apply:cprodb_exten => x xc; rewrite LgV //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)