Definition rcanfromrinv (a b c : X) (c' : hasrinv opp is c) : a * c = b * c → a = b. Proof. intros e. refine (!runax_is is a @ _ @ runax_is is b). refine (!maponpaths (λ z, _ * z) (pr2 c') @ _ @ maponpaths (λ z, _ * z) (pr2 c')). refine (!assocax_is is _ _ _ @ _ @ assocax_is is _ _ _). apply (maponpaths (λ z, z * _)). assumption. Defined.