proposition: Lemma weqhrelhrel0commringfrac (X : commring) (S : @submonoid (ringmultabmonoid X)) (iscanc : ∏ a : S, isrcancelable (@op2 X) (pr1carrier _ a)) (xa xa' : dirprod X S) : (eqrelcommringfrac X S xa xa') ≃ (hrelcommringfrac0 X S xa xa').
proof: Proof. intros. unfold eqrelabmonoidfrac. unfold hrelabmonoidfrac. simpl. apply weqimplimpl. - apply (@hinhuniv _ (_ = _)). intro ae. destruct ae as [ a eq ]. apply (invmaponpathsincl _ (iscanc a) _ _ eq). - intro eq. apply hinhpr. split with (unel S). rewrite (ringrunax2 X). rewrite (ringrunax2 X). apply eq. - apply (isapropishinh _). - apply (setproperty X). Defined.
imports: UniMath.Algebra.Groups UniMath.MoreFoundations.Sets UniMath.MoreFoundations.Orders UniMath.Algebra.Monoids