Lemma inverse_in_submonoid (X : monoid) : ∏ (x x0 : X), merely_invertible_elements (@op X) (pr2 X) x → isinvel (@op X) (pr2 X) x x0 → merely_invertible_elements (@op X) (pr2 X) x0. Proof. intros x x0 _ x0isxinv. unfold merely_invertible_elements, hasinv. apply hinhpr. exact (x,, is_inv_inv (@op X) _ _ _ x0isxinv). Defined.
Require Import UniMath.MoreFoundations.Subtypes. Require Import UniMath.MoreFoundations.Sets.