Lemma invop : ∏ (x y x' y' : X), (isinvel x x' → isinvel y y' → isinvel (x * y) (y' * x')). 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.