proposition: Lemma binn n : 'C(n, n) = 1.
proof: Proof. by elim: n => [// |n IHn]; rewrite binS bin_small. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype) mathcomp(ssrnat seq path div) mathcomp(fintype tuple finfun bigop finset binomial)