proposition: Lemma invop_r : ∏ (x y x' y' : X), (isrinvel x x' -> isrinvel y y' -> isrinvel (x * y) (y' * x')).
proof: 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.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions