proposition: Lemma aput_writeList_rcons i x h (t : seq E) : aput i x >> writeList i.+1 (rcons t h) = aput i h >> ((writeList i.+1 t >> aput (i + (size t).+1) x) >> aswap i (i + (size t).+1)).
proof: Proof. rewrite /aswap -!bindA writeList_rcons -bindA. rewrite aput_writeListC// aput_writeListC// !bindA; bind_ext => -[]. under [RHS] eq_bind do rewrite -bindA. rewrite aputgetC; last by rewrite gtn_eqF// -addSnnS ltn_addr. rewrite -bindA aputget. under [RHS] eq_bind do rewrite -!bindA. rewrite aputget aputC; last by right. by rewrite -!bindA aputput bindA aputput -addSnnS. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib