proposition: Lemma last_mkseq (T : Type) (f: nat -> T) a b c: last c [seq f i | i <- iota a b.+1] = f (a + b).
proof: Proof. by rewrite iota_Sr map_rcons last_rcons. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(seq path fintype div bigop binomial) mathcomp(prime finset ssralg ssrnum ssrint)