proposition: Lemma fastprodE s : fastprod s = Ret (product s).
proof: Proof. rewrite /fastprod /work fun_if if_arg catchfailm. by rewrite catchret; case: ifPn => // /product0 <-. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)