proposition: Lemma product0 s : O \in s -> product s = O.
proof: Proof. elim: s => //= h t ih; rewrite inE => /orP[/eqP <-|/ih ->]; by rewrite ?muln0 ?mul0n. Qed.
imports: mathcomp(all_ssreflect) imonae_lib HB(structures) ihierarchy imonad_lib Equations(Equations)