proposition: Lemma triangular_sum n : \sum_(0 <= i < n) i = 'C(n, 2).
proof: Proof. elim: n => [|n IHn]; first by rewrite big_geq. by rewrite big_nat_recr // IHn binS bin1. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)