proposition: Lemma fastProductCorrect l n : evalStateT (fastProduct l) n = Ret (product l).
proof: Proof. rewrite /fastProduct -(mul1n (product _)); move: 1. elim: l => [ | [ | x] l ih] m. - rewrite muln1 bindA bindretf putget. rewrite /evalStateT runStateTcatch runStateTbind runStateTput bindretf. by rewrite runStateTret runStateTret catchret bindretf. - rewrite muln0. rewrite /evalStateT runStateTcatch runStateTbind runStateTbind runStateTput. by rewrite bindretf runStateTfail bindfailf catchfailm runStateTret bindretf. - rewrite [fastProductRec _]/=. by rewrite -bindA putget bindA bindA bindretf -bindA -bindA putput ih mulnA. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib monad_transformer