proposition: Lemma sum_char2 (F : fieldType) (_ : 2%N \in [char F]) k (f : 'I_k -> F) : (\sum_(i < k) (f i)) ^+ 2 = \sum_(i < k) (f i) ^+ 2.
proof: Proof. elim/big_ind2 : _ => [|x1 x2 y1 y2 <- <-|//] /=; first by rewrite expr0n. by rewrite sqrrD mulr2n addrr_char2 // addr0. Qed.
imports: mathcomp(all_ssreflect ssralg fingroup finalg perm zmodp) mathcomp(matrix mxalgebra vector) ssr_ext f2