proposition: Lemma sum1_size J (r : seq J) : \sum_(j <- r) 1 = size r.
proof: Proof. by rewrite sum1_count count_predT. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div fintype tuple finfun)