proposition: Lemma sum_test n : sum n = get >>= (fun m => put (m + sumn (iota 0 n))).
proof: Proof. elim: n => [|n ih]. rewrite /sum. rewrite loop0. rewrite (_ : sumn (iota 0 0) = 0) //. rewrite -[LHS]bindskipf. rewrite -getputskip. rewrite bindA. bind_ext => a. rewrite addn0. rewrite -[RHS]bindmret. bind_ext. by case. rewrite {1}/sum -add1n loop1 bindA; bind_ext => m. rewrite -/(sum n) {}ih -bindA putget bindA bindretf putput. congr put. by rewrite add0n (addnC 1) iotaD /= sumn_cat /= add0n addn0 /= addnAC addnA. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib fail_lib