Definition one_intdomnonzerosubmonoid : intdomnonzerosubmonoid hzintdom. Proof. exists 1%hz ; simpl. exact hzone_neg_hzzero. Defined.
Require Import UniMath.Foundations.Preamble. Require Import UniMath.MoreFoundations.Tactics.