proposition: Lemma ipartl_guard p i ny nz nx : ipartl (M := M) p i ny nz nx = ipartl p i ny nz nx >>= (fun '(a, b) => (guard ((a <= nx + ny + nz) && (b <= nx + ny + nz))%N >> Ret (a, b))).
proof: Proof. elim: nx ny nz => [ny nz|n ih ny nz]. by rewrite /= bindretf add0n leq_addr leq_addl guardT bindskipf. rewrite /= [in RHS]bindA; bind_ext => x; case: ifPn => xp. - rewrite [in RHS]bindA; bind_ext => -[]; rewrite [in LHS]ih. by under eq_bind do rewrite -addSnnS. - rewrite [in LHS]ih. by under [in RHS]eq_bind do rewrite addSnnS -addnA addSnnS addnA. Qed.
imports: mathcomp(all_ssreflect) monae_lib hierarchy monad_lib fail_lib state_lib array_lib example_quicksort infotheo(ssr_ext)