proposition: Lemma cpow1x a: \1c ^c a = \1c.
proof: Proof. move: fgraph_set0 domain_set0 => eg de. by rewrite - (cprod_trivial de) cpow_prod // de /cprodb /Lg funI_set0. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)