Lemma isaprop_istruncminus {X : abmonoid} (lat : lattice X) (minus : binop X) : isaprop (istruncminus lat minus). Proof. apply impred_isaprop ; intros x. apply impred_isaprop ; intros y. apply setproperty. Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.