proposition: Lemma F5aux n: \sum_(i<n) i = 'C(n,2).
proof: Proof. transitivity (\sum_(i<n) i ^1); first by apply:eq_bigr => //. rewrite sum_pow ! big_ord_recr /= big_ord0 mul0n mul1n //. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)