proposition: Lemma is_iota_head_last s : is_iota s -> 0 < size s -> head 0 s + size s = (last 0 s).+1.
proof: Proof. elim: s => //= a [_ /=|c d IH]. by rewrite addn1. rewrite /is_iota /= => /eqP[] ?; subst c => Hd _. rewrite /= in IH. by rewrite -IH // -?addSnnS // /is_iota /= -Hd. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib