Definition isaprop_hasrinv (x : X) (can : isrcancelable opp x) : isaprop (haslinv opp is x). Proof. apply isaproptotal2. - intro; apply isapropisrinvel. - intros x' x'' isrinvx' isrinvx''. apply (Injectivity (λ x0 : X, x0 * x)). + apply incl_injectivity; assumption. + exact (isrinvx' @ !isrinvx''). Defined.