proposition: Lemma binE n m : binomial n m = match n, m with | n'.+1, m'.+1 => binomial n' m + binomial n' m' | _, 0 => 1 | 0, _.+1 => 0 end.
proof: Proof. by case: n. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq path) mathcomp(div fintype tuple finfun bigop prime finset)