Lemma isaprop_in_same_right_coset (x1 x2 : X) : isaprop (in_same_right_coset Y x1 x2). Proof. 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, y * x1 = x2). pose (q' := (pr11 q,, pr2 q) : ∑ y : X, y * x1 = x2). apply (maponpaths pr1 (iscontrpr1 (isaprop_mult_eq_l _ _ p' q'))). Defined.
Require Import UniMath.MoreFoundations.Subtypes.