Lemma isaprop_extruncminus {X : abmonoid} (lat : lattice X) (Hop : isrcancellative (@op X)) : isaprop (extruncminus lat). Proof. intros minus1 minus2 ; simpl. apply iscontraprop1. - apply isaset_total2. apply impred_isaset ; intros _. apply impred_isaset ; intros _. apply setproperty. intros minus. apply isasetaprop. apply isaprop_istruncminus. - apply subtypePath. + intros f. apply isaprop_istruncminus. + apply weqfunextsec ; intros x. apply weqfunextsec ; intros y. eapply rcancel. { apply Hop. } rewrite (pr2 minus1). apply pathsinv0, (pr2 minus2). Qed.
Require Import UniMath.MoreFoundations.All. Require Import UniMath.Algebra.Monoids. Require Import UniMath.Algebra.Groups.