proposition: Lemma nth_iota p m n i : i < n -> nth p (iota m n) i = m + i.
proof: Proof. by move/subnKC <-; rewrite addSnnS iotaD nth_cat size_iota ltnn subnn. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)