Lemma isaprop_in_same_left_coset (x1 x2 : X) : isaprop (in_same_left_coset Y x1 x2). Proof. unfold in_same_left_coset. apply invproofirrelevance; intros p q. apply subtypePath. { intros x'. apply setproperty. } apply subtypePath. { intros x'. apply propproperty. } pose (p' := (pr11 p,, pr2 p) : ∑ y : X, x1 * y = x2). pose (q' := (pr11 q,, pr2 q) : ∑ y : X, x1 * y = x2). apply (maponpaths pr1 (iscontrpr1 (isaprop_mult_eq_r _ _ p' q'))). Defined.
Require Import UniMath.MoreFoundations.Subtypes.