Definition isaprop_haslinv (x : X) (can : islcancelable opp x) : isaprop (hasrinv opp is x). Proof. apply isaproptotal2. - intro; apply isapropislinvel. - intros x' x'' islinvx' islinvx''. apply (Injectivity (λ x0 : X, x * x0)). + apply incl_injectivity; assumption. + exact (islinvx' @ !islinvx''). Defined.