proposition: Lemma plus_commute A (m : M A) B (n : M B) C (f : A -> B -> M C) : plus_isNondet m -> commute m n f.
proof: Proof. case=> x; elim: x m n f => [{}A a m n f <-| D {}A n0 ih0 n1 ih1 m n2 f <- | D m n f <- | D n0 ih0 n1 ih1 m n2 f <-]. - rewrite /commute bindretf. by under [RHS]eq_bind do rewrite bindretf. - rewrite /commute /= bindA. under eq_bind. move=> x; rewrite (ih1 x) //. over. by rewrite ih0 //; under eq_bind do rewrite -bindA. - rewrite /commute /= bindfailf. under eq_bind do rewrite bindfailf. by rewrite bindmfail. - rewrite /commute /= alt_bindDl. under [RHS]eq_bind do rewrite alt_bindDl. by rewrite alt_bindDr ih0 // ih1. Qed.
imports: mathcomp(all_ssreflect) monae_lib HB(structures) hierarchy monad_lib Equations(Equations)