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