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