proposition: Lemma lcnSn n A : 'L_n.+2(A) = [~: 'L_n.+1(A), A].
proof: Proof. by []. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(fintype div bigop prime finset fingroup morphism) mathcomp(automorphism quotient commutator gproduct) mathcomp(gfunctor center gseries cyclic)