proposition: Theorem cprod_of_same a b: cprodb b (fun i: Set => a) = a ^c b.
proof: Proof. rewrite cpow_pr0 /cprodb /cprod (setXb_eq_gfunctions (x:=a)); aw; trivial. by move => i ib; rewrite LgV. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)