proposition: 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: Proof. intros x x0 _ x0isxinv. unfold merely_invertible_elements, hasinv. apply hinhpr. exact (x,, is_inv_inv (@op X) _ _ _ x0isxinv). Defined.
imports: UniMath.Algebra.BinaryOperations UniMath.MoreFoundations.Subtypes UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders