proposition: Lemma F5aux2 n: \sum_(i<n) i = 'C(n,2).
proof: Proof. by elim: n => [| n Hn]; [ rewrite big_ord0 | rewrite big_ord_recr Hn binS bin1]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)