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