proposition: Lemma invop : ∏ (x y x' y' : X), (isinvel x x' -> isinvel y y' -> isinvel (x * y) (y' * x')).
proof: Proof. intros x y x' y' xinv yinv. use make_dirprod. - apply invop_l. + exact (dirprod_pr1 xinv). + exact (dirprod_pr1 yinv). - apply invop_r. + exact (dirprod_pr2 xinv). + exact (dirprod_pr2 yinv). Defined.
imports: UniMath.Foundations.Sets UniMath.MoreFoundations.Propositions