fact: Definition swap {S : UU0} {I : eqType} {M : arrayMonad S I} (i j : I) : M unit := (do x <- aget i ; do y <- aget j ; aput i y >> aput j x)%Do.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib ifail_lib