Definition isaprop_hasinv (x : X) (can : iscancelable opp x) : isaprop (hasinv opp is x). Proof. apply isaproptotal2. - intro; apply isapropdirprod. + apply isapropislinvel. + apply isapropisrinvel. - intros x' x'' isinvx' isinvx''. apply (Injectivity (λ x0 : X, x * x0)). + apply incl_injectivity; apply (pr1 can). + exact (pr2 isinvx' @ !pr2 isinvx''). Defined.