proposition: Lemma expMg_Rmul : (y * x) ^+ i = y ^+ i * x ^+ i * [~ x, y] ^+ 'C(i, 2).
proof: Proof. rewrite -triangular_sum; symmetry. elim: i => [|k IHk] /=; first by rewrite big_geq ?mulg1. rewrite big_nat_recr //= addnC expgD !expgS -{}IHk !mulgA; congr (_ * _). by rewrite -!mulgA commuteX2 // -commgX // [mulg y]lock 3!mulgA -commgC. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat fintype) mathcomp(bigop finset binomial fingroup morphism) mathcomp(automorphism quotient gfunctor)