Lemma mere_invop : ∏ (x y : X), (merely_hasinv x → merely_hasinv y → merely_hasinv (x * y)). Proof. intros x y. apply hinhfun2. intros xinv yinv. exists ((hasinv_to_invel yinv) * (hasinv_to_invel xinv)). apply invop. - exact (pr2 xinv). - exact (pr2 yinv). Defined.