proposition: Lemma textbook_triangular_sum n : \sum_(0 <= i < n) i = 'C(n, 2).
proof: Proof. rewrite bin2; apply: canRL half_double _. rewrite -addnn {1}big_nat_rev -big_split big_mkord /= ?add0n. rewrite (eq_bigr (fun _ => n.-1)); first by rewrite sum_nat_const card_ord. by case: n => [|n] [i le_i_n] //=; rewrite subSS subnK. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)