proposition: Lemma binomial_sumn_iota n : 'C(n, 2) = sumn (iota 0 n).
proof: Proof. by rewrite -triangular_sum sumnE /index_iota subn0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun ssrnat eqtype fintype choice seq) mathcomp(finset bigop path binomial)