proposition: Lemma prod_constt x : \prod_(0 <= p < #[x].+1) x.`_p = x.
proof: Proof. pose lp n := [pred p | p < n]. have: (lp #[x].+1).-elt x by apply/pnatP=> // p _; apply: dvdn_leq. move/constt_p_elt=> def_x; symmetry; rewrite -{1}def_x {def_x}. elim: _.+1 => [|p IHp]. by rewrite big_nil; apply/constt1P; apply/pgroupP. rewrite big_nat_recr //= -{}IHp -(consttC (lp p) x.`__); congr (_ * _). by rewrite sub_in_constt // => q _; apply: leqW. set y := _.`__; rewrite -(consttC p y) (constt1P p^' _ _) ?mulg1. by rewrite 2?sub_in_constt // => q _; move/eqnP->; rewrite !inE ?ltnn. rewrite /p_elt pnatNK !order_constt -partnI. apply: sub_in_pnat (part_pnat _ _) => q _. by rewrite !inE ltnS -leqNgt -eqn_leq. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop finset prime fingroup morphism) mathcomp(gfunctor automorphism quotient action gproduct) mathcomp(cyclic)