proposition: Lemma F1 x y n: (\sum_(i<n.+1) (x+y*+ i))*+2 = (x*+2+y*+n)*+n.+1.
proof: Proof. elim: n; first by rewrite big_ord_recl big_ord0 mulr1n mulr0n !addr0. move => n Hrec. rewrite big_ord_recr /= mulrnDl Hrec mulrnDl - !mulrnA mulrnDl - !mulrnA. rewrite addrAC addrA - mulrnDr - addrA -mulrnDr mulrnDl - !mulrnA -(addn1 n.+1). congr ((x *+ _) + (y *+ _)). rewrite mulnDr //. rewrite mulnC - mulnDl add2n addn1 mulnC//. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq choice fintype binomial) mathcomp(bigop ssralg poly ssrint) gaia(ssete7)