Definition natnonzero : @subabmonoid natmultabmonoid. Proof. split with (λ a : natset, a ≠ 0). unfold issubmonoid. split. - unfold issubsetwithbinop. intros a a'. apply (natneq0andmult _ _ (pr2 a) (pr2 a')). - apply (ct (natneq, isdecrel_natneq, 1, 0)). Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.NegativePropositions.