Lemma invop_l : ∏ (x y x' y' : X), (islinvel x x' → islinvel y y' → islinvel (x * y) (y' * x')). Proof. intros x y x' y' xinv yinv. unfold islinvel. pose (assoc := pr1 is). cbn; unfold islinvel. rewrite <- assoc. rewrite (assoc4 opp assoc), xinv. rewrite (runax_is is). exact yinv. Qed.