proposition: Lemma prod4 : Prod.prod4 (@prod).
proof: Proof. move=> A; rewrite {1}/Prod.JOIN -JOIN_prod JOIN_dorp {1}/prod (@functor_o N). rewrite (compA (M # Join \o swap)) -(compA (_ # Join)) Hswap1. rewrite (compA (M # Join)) -functor_o joinA functor_o. rewrite -[LHS]compA -(compA (_ # Join)) (compA (M # Join) swap) -/prod Hswap4. by rewrite [LHS]compA /Prod.JOIN -JOIN_prod JOIN_dorp. Qed.
imports: mathcomp(all_ssreflect) HB(structures) monae_lib hierarchy monad_lib