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