Require Import Basics.Overture Basics.Trunc Basics.Tactics Colimits.QuotientRequire Import Basics.Overture Basics.Trunc Basics.Tactics Colimits.Quotient
  abstract_algebra Rings.CRing Truncations.Core Nat.Core
  Rings.QuotientRing WildCat.Core WildCat.Equiv.

Local Open Scope mc_scope.

(** * Localization of commutative rings *)

(** Localization is a way to make elements in a commutative ring invertible by adding inverses, in the most minimal way possible. It generalizes the familiar operation of a field of fractions. *)

(** ** Multiplicative subsets *)

(** A multiplicative subset is formally a submonoid of the multiplicative monoid of a ring. Essentially it is a subset closed under finite products. *)

(** *** Definition *)

(** Multiplicative subsets of a ring [R] consist of: *)
Class IsMultiplicativeSubset {R : CRing} (S : R -> Type) : Type := {
  (** Contains one *)
  mss_one : S 1 ;
  (** Closed under multiplication *)
  mss_mult : forall x y, S x -> S y -> S (x * y) ;
}.

Arguments mss_one {R _ _}.
Arguments mss_mult {R _ _ _ _}.

(** *** Examples *)

(** The multiplicative subset of powers of a ring element. *)
Instance ismultiplicative_powers (R : CRing) (x : R)
  : IsMultiplicativeSubset (fun r => exists n, rng_power x n = r).
R: CRing
x: R
IsMultiplicativeSubset (fun r : R => {n : nat & rng_power x n = r})
Proof.
R: CRing
x: R
IsMultiplicativeSubset (fun r : R => {n : nat & rng_power x n = r})
  srapply Build_IsMultiplicativeSubset; cbn beta.
R: CRing
x: R
{n : nat & rng_power x n = 1}
R: CRing
x: R
forall x0 y : R,
{n : nat & rng_power x n = x0} ->
{n : nat & rng_power x n = y} -> {n : nat & rng_power x n = x0 * y}
  1: by exists 0%nat.
R: CRing
x: R
forall x0 y : R,
{n : nat & rng_power x n = x0} ->
{n : nat & rng_power x n = y} -> {n : nat & rng_power x n = x0 * y}
  intros a b np mq.
R: CRing
x, a, b: R
np: {n : nat & rng_power x n = a}
mq: {n : nat & rng_power x n = b}
{n : nat & rng_power x n = a * b}
  destruct np as [n p], mq as [m q].
R: CRing
x, a, b: R
n: nat
p: rng_power x n = a
m: nat
q: rng_power x m = b
{n0 : nat & rng_power x n0 = a * b}
  exists (n + m)%nat.
R: CRing
x, a, b: R
n: nat
p: rng_power x n = a
m: nat
q: rng_power x m = b
rng_power x (n + m) = a * b
  lhs_V napply rng_power_mult_law.
R: CRing
x, a, b: R
n: nat
p: rng_power x n = a
m: nat
q: rng_power x m = b
rng_power x n * rng_power x m = a * b
  f_ap.
Defined.

(** Invertible elements of a ring form a multiplicative subset. *)
Instance ismultiplicative_isinvertible (R : CRing)
  : IsMultiplicativeSubset (@IsInvertible R) := {}.

(** TODO: Property of being a localization. *)

(** ** Construction of localization *)

Section Localization.

  (** We now construct the localization of a ring at a multiplicative subset as the following HIT:

<<
  HIT (Quotient fraction_eq) (R : CRing) (S : R -> Type)
    `{IsMultiplicativeSubset R} :=
  | loc_frac (n d : R) (p : S d) : Localization R S
  | loc_frac_eq (n1 d1 n2 d2 : R) (p1 : S d1) (p2 : S d2)
      (x : R) (q : S x) (r : x * (d2 * n1 - n2 * d1) = 0)
      : loc_frac n1 d1 p1 = loc_frac n2 d2 p2
  .
>>

  along with the condition that this HIT be a set.

  We will implement this HIT by writing it as a set quotient. From now on, [loc_frac] will be implemented as [class_of fraction_eq] and [loc_frac_eq] will be implemented as [qglue]. *)

  Context (R : CRing) (S : R -> Type) `{!IsMultiplicativeSubset S}.

  (** *** Construction of underlying Localization type *)

  (** The base type will be the type of fractions with respect to a multiplicative subset. This consists of pairs of elements of a ring [R] where the [denominator] is in the multiplicative subset [S]. *)
  Record Fraction := {
    numerator : R ;
    denominator : R ;
    in_mult_subset_denominator : S denominator ;
  }.

  (** We consider two fractions to be equal if we can rearrange the fractions as products and ask for equality up to some scaling factor from the multiplicative subset [S]. *)
  Definition fraction_eq : Relation Fraction.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Relation Fraction
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Relation Fraction
    intros [n1 d1 ?] [n2 d2 ?].
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
n1, d1: R
in_mult_subset_denominator0: S d1
n2, d2: R
in_mult_subset_denominator1: S d2
Type
    refine (exists (x : R), S x /\ _).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
n1, d1: R
in_mult_subset_denominator0: S d1
n2, d2: R
in_mult_subset_denominator1: S d2
x: R
Type
    exact (x * n1 * d2 = x * n2 * d1).
  Defined.

  (** It is convenient to produce elements of this relation specialized to when the scaling factor is [1]. *)
  Definition fraction_eq_simple f1 f2
    (p : numerator f1 * denominator f2 = numerator f2 * denominator f1)
    : fraction_eq f1 f2.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2: Fraction
p: numerator f1 * denominator f2 = numerator f2 * denominator f1
fraction_eq f1 f2
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2: Fraction
p: numerator f1 * denominator f2 = numerator f2 * denominator f1
fraction_eq f1 f2
    exists 1.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2: Fraction
p: numerator f1 * denominator f2 = numerator f2 * denominator f1
S 1 * (1 * numerator f1 * denominator f2 = 1 * numerator f2 * denominator f1)
    refine (mss_one, _).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2: Fraction
p: numerator f1 * denominator f2 = numerator f2 * denominator f1
1 * numerator f1 * denominator f2 = 1 * numerator f2 * denominator f1
    lhs_V napply rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2: Fraction
p: numerator f1 * denominator f2 = numerator f2 * denominator f1
1 * (numerator f1 * denominator f2) = 1 * numerator f2 * denominator f1
    rhs_V napply rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2: Fraction
p: numerator f1 * denominator f2 = numerator f2 * denominator f1
1 * (numerator f1 * denominator f2) = 1 * (numerator f2 * denominator f1)
    exact (ap (1 *.) p).
  Defined.

  (** Fraction equality is a reflexive relation. *)
  Definition fraction_eq_refl f1 : fraction_eq f1 f1.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1: Fraction
fraction_eq f1 f1
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1: Fraction
fraction_eq f1 f1
    apply fraction_eq_simple.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1: Fraction
numerator f1 * denominator f1 = numerator f1 * denominator f1
    reflexivity.
  Defined.

  (** Elements of [R] can be considered fractions. *)
  Definition frac_in : R -> Fraction
    := fun r => Build_Fraction r 1 mss_one.

  (** Now that we have defined the HIT as above, we can define the ring structure. *)

  (** *** Addition operation *)

  (** Fraction addition is the usual addition of fractions. *)
  Definition frac_add : Fraction -> Fraction -> Fraction :=
    fun '(Build_Fraction n1 d1 p1) '(Build_Fraction n2 d2 p2)
      => Build_Fraction (n1 * d2 + n2 * d1) (d1 * d2) (mss_mult p1 p2).

  (** Fraction addition is well-defined up to equality of fractions. *)

  (** It is easier to prove well-definedness as a function of both arguments at once. *)
  Definition frac_add_wd (f1 f1' f2 f2' : Fraction)
    (p : fraction_eq f1 f1') (q : fraction_eq f2 f2')
    : fraction_eq (frac_add f1 f2) (frac_add f1' f2').
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f1', f2, f2': Fraction
p: fraction_eq f1 f1'
q: fraction_eq f2 f2'
fraction_eq (frac_add f1 f2) (frac_add f1' f2')
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f1', f2, f2': Fraction
p: fraction_eq f1 f1'
q: fraction_eq f2 f2'
fraction_eq (frac_add f1 f2) (frac_add f1' f2')
    destruct f1 as [a s ss], f1' as [a' s' ss'],
      f2 as [b t st], f2' as [b' t' st'],
      p as [x [sx p]], q as [y [sy q]].
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
a, s: R
ss: S s
a', s': R
ss': S s'
b, t: R
st: S t
b', t': R
st': S t'
x: R
sx: S x
p: x * a * s' = x * a' * s
y: R
sy: S y
q: y * b * t' = y * b' * t
fraction_eq
  (frac_add
     {| numerator := a; denominator := s; in_mult_subset_denominator := ss |}
     {| numerator := b; denominator := t; in_mult_subset_denominator := st |})
  (frac_add
     {|
       numerator := a'; denominator := s'; in_mult_subset_denominator := ss'
     |}
     {|
       numerator := b'; denominator := t'; in_mult_subset_denominator := st'
     |})
    refine (x * y ; (mss_mult sx sy, _)).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
a, s: R
ss: S s
a', s': R
ss': S s'
b, t: R
st: S t
b', t': R
st': S t'
x: R
sx: S x
p: x * a * s' = x * a' * s
y: R
sy: S y
q: y * b * t' = y * b' * t
x * y *
numerator
  (frac_add
     {| numerator := a; denominator := s; in_mult_subset_denominator := ss |}
     {| numerator := b; denominator := t; in_mult_subset_denominator := st |}) *
denominator
  (frac_add
     {|
       numerator := a'; denominator := s'; in_mult_subset_denominator := ss'
     |}
     {|
       numerator := b'; denominator := t'; in_mult_subset_denominator := st'
     |}) =
x * y *
numerator
  (frac_add
     {|
       numerator := a'; denominator := s'; in_mult_subset_denominator := ss'
     |}
     {|
       numerator := b'; denominator := t'; in_mult_subset_denominator := st'
     |}) *
denominator
  (frac_add
     {| numerator := a; denominator := s; in_mult_subset_denominator := ss |}
     {| numerator := b; denominator := t; in_mult_subset_denominator := st |})
    simpl.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
a, s: R
ss: S s
a', s': R
ss': S s'
b, t: R
st: S t
b', t': R
st': S t'
x: R
sx: S x
p: x * a * s' = x * a' * s
y: R
sy: S y
q: y * b * t' = y * b' * t
x * y * (a * t + b * s) * (s' * t') = x * y * (a' * t' + b' * s') * (s * t)
    rewrite 2 rng_dist_l, 2 rng_dist_r.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
a, s: R
ss: S s
a', s': R
ss': S s'
b, t: R
st: S t
b', t': R
st': S t'
x: R
sx: S x
p: x * a * s' = x * a' * s
y: R
sy: S y
q: y * b * t' = y * b' * t
x * y * (a * t) * (s' * t') + x * y * (b * s) * (s' * t') =
x * y * (a' * t') * (s * t) + x * y * (b' * s') * (s * t)
    snapply (ap011 (+)).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
a, s: R
ss: S s
a', s': R
ss': S s'
b, t: R
st: S t
b', t': R
st': S t'
x: R
sx: S x
p: x * a * s' = x * a' * s
y: R
sy: S y
q: y * b * t' = y * b' * t
x * y * (a * t) * (s' * t') = x * y * (a' * t') * (s * t)
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
a, s: R
ss: S s
a', s': R
ss': S s'
b, t: R
st: S t
b', t': R
st': S t'
x: R
sx: S x
p: x * a * s' = x * a' * s
y: R
sy: S y
q: y * b * t' = y * b' * t
x * y * (b * s) * (s' * t') = x * y * (b' * s') * (s * t) 
    -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
a, s: R
ss: S s
a', s': R
ss': S s'
b, t: R
st: S t
b', t': R
st': S t'
x: R
sx: S x
p: x * a * s' = x * a' * s
y: R
sy: S y
q: y * b * t' = y * b' * t
x * y * (a * t) * (s' * t') = x * y * (a' * t') * (s * t) rewrite 4 rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
a, s: R
ss: S s
a', s': R
ss': S s'
b, t: R
st: S t
b', t': R
st': S t'
x: R
sx: S x
p: x * a * s' = x * a' * s
y: R
sy: S y
q: y * b * t' = y * b' * t
x * y * a * t * s' * t' = x * y * a' * t' * s * t
      rewrite 8 (rng_mult_permute_2_3 _ y).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
a, s: R
ss: S s
a', s': R
ss': S s'
b, t: R
st: S t
b', t': R
st': S t'
x: R
sx: S x
p: x * a * s' = x * a' * s
y: R
sy: S y
q: y * b * t' = y * b' * t
x * a * t * s' * t' * y = x * a' * t' * s * t * y
      apply (ap (.* y)).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
a, s: R
ss: S s
a', s': R
ss': S s'
b, t: R
st: S t
b', t': R
st': S t'
x: R
sx: S x
p: x * a * s' = x * a' * s
y: R
sy: S y
q: y * b * t' = y * b' * t
x * a * t * s' * t' = x * a' * t' * s * t
      rewrite 2 (rng_mult_permute_2_3 _ t).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
a, s: R
ss: S s
a', s': R
ss': S s'
b, t: R
st: S t
b', t': R
st': S t'
x: R
sx: S x
p: x * a * s' = x * a' * s
y: R
sy: S y
q: y * b * t' = y * b' * t
x * a * s' * t' * t = x * a' * t' * s * t
      apply (ap (.* t)).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
a, s: R
ss: S s
a', s': R
ss': S s'
b, t: R
st: S t
b', t': R
st': S t'
x: R
sx: S x
p: x * a * s' = x * a' * s
y: R
sy: S y
q: y * b * t' = y * b' * t
x * a * s' * t' = x * a' * t' * s
      rewrite (rng_mult_permute_2_3 _ t').
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
a, s: R
ss: S s
a', s': R
ss': S s'
b, t: R
st: S t
b', t': R
st': S t'
x: R
sx: S x
p: x * a * s' = x * a' * s
y: R
sy: S y
q: y * b * t' = y * b' * t
x * a * s' * t' = x * a' * s * t'
      f_ap.
    -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
a, s: R
ss: S s
a', s': R
ss': S s'
b, t: R
st: S t
b', t': R
st': S t'
x: R
sx: S x
p: x * a * s' = x * a' * s
y: R
sy: S y
q: y * b * t' = y * b' * t
x * y * (b * s) * (s' * t') = x * y * (b' * s') * (s * t) do 2 lhs_V napply rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
a, s: R
ss: S s
a', s': R
ss': S s'
b, t: R
st: S t
b', t': R
st': S t'
x: R
sx: S x
p: x * a * s' = x * a' * s
y: R
sy: S y
q: y * b * t' = y * b' * t
x * (y * (b * s * (s' * t'))) = x * y * (b' * s') * (s * t)
      do 2 rhs_V napply rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
a, s: R
ss: S s
a', s': R
ss': S s'
b, t: R
st: S t
b', t': R
st': S t'
x: R
sx: S x
p: x * a * s' = x * a' * s
y: R
sy: S y
q: y * b * t' = y * b' * t
x * (y * (b * s * (s' * t'))) = x * (y * (b' * s' * (s * t)))
      f_ap.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
a, s: R
ss: S s
a', s': R
ss': S s'
b, t: R
st: S t
b', t': R
st': S t'
x: R
sx: S x
p: x * a * s' = x * a' * s
y: R
sy: S y
q: y * b * t' = y * b' * t
y * (b * s * (s' * t')) = y * (b' * s' * (s * t))
      rewrite 6 rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
a, s: R
ss: S s
a', s': R
ss': S s'
b, t: R
st: S t
b', t': R
st': S t'
x: R
sx: S x
p: x * a * s' = x * a' * s
y: R
sy: S y
q: y * b * t' = y * b' * t
y * b * s * s' * t' = y * b' * s' * s * t
      rewrite 2 (rng_mult_permute_2_3 _ _ t').
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
a, s: R
ss: S s
a', s': R
ss': S s'
b, t: R
st: S t
b', t': R
st': S t'
x: R
sx: S x
p: x * a * s' = x * a' * s
y: R
sy: S y
q: y * b * t' = y * b' * t
y * b * t' * s * s' = y * b' * s' * s * t
      rewrite 2 (rng_mult_permute_2_3 _ _ t).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
a, s: R
ss: S s
a', s': R
ss': S s'
b, t: R
st: S t
b', t': R
st': S t'
x: R
sx: S x
p: x * a * s' = x * a' * s
y: R
sy: S y
q: y * b * t' = y * b' * t
y * b * t' * s * s' = y * b' * t * s' * s
      lhs_V napply rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
a, s: R
ss: S s
a', s': R
ss': S s'
b, t: R
st: S t
b', t': R
st': S t'
x: R
sx: S x
p: x * a * s' = x * a' * s
y: R
sy: S y
q: y * b * t' = y * b' * t
y * b * t' * (s * s') = y * b' * t * s' * s
      rhs_V napply rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
a, s: R
ss: S s
a', s': R
ss': S s'
b, t: R
st: S t
b', t': R
st': S t'
x: R
sx: S x
p: x * a * s' = x * a' * s
y: R
sy: S y
q: y * b * t' = y * b' * t
y * b * t' * (s * s') = y * b' * t * (s' * s)
      f_ap; apply rng_mult_comm.
  Defined.

  Definition frac_add_wd_l (f1 f1' f2 : Fraction) (p : fraction_eq f1 f1')
    : fraction_eq (frac_add f1 f2) (frac_add f1' f2).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f1', f2: Fraction
p: fraction_eq f1 f1'
fraction_eq (frac_add f1 f2) (frac_add f1' f2)
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f1', f2: Fraction
p: fraction_eq f1 f1'
fraction_eq (frac_add f1 f2) (frac_add f1' f2)
    pose (fraction_eq_refl f2).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f1', f2: Fraction
p: fraction_eq f1 f1'
f:= fraction_eq_refl f2: fraction_eq f2 f2
fraction_eq (frac_add f1 f2) (frac_add f1' f2)
    by apply frac_add_wd.
  Defined.

  Definition frac_add_wd_r (f1 f2 f2' : Fraction) (p : fraction_eq f2 f2')
    : fraction_eq (frac_add f1 f2) (frac_add f1 f2').
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2, f2': Fraction
p: fraction_eq f2 f2'
fraction_eq (frac_add f1 f2) (frac_add f1 f2')
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2, f2': Fraction
p: fraction_eq f2 f2'
fraction_eq (frac_add f1 f2) (frac_add f1 f2')
    pose (fraction_eq_refl f1).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2, f2': Fraction
p: fraction_eq f2 f2'
f:= fraction_eq_refl f1: fraction_eq f1 f1
fraction_eq (frac_add f1 f2) (frac_add f1 f2')
    by apply frac_add_wd.
  Defined.

  (** The addition operation on the localization is induced from the addition operation for fractions. *)
  Instance plus_rng_localization : Plus (Quotient fraction_eq).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Plus (Quotient fraction_eq)
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Plus (Quotient fraction_eq)
    srapply Quotient_rec2.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Fraction -> Fraction -> Quotient fraction_eq
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
forall a a' b : Fraction, fraction_eq a a' -> ?dclass a b = ?dclass a' b
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
forall a b b' : Fraction, fraction_eq b b' -> ?dclass a b = ?dclass a b'
    -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Fraction -> Fraction -> Quotient fraction_eq cbn.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Fraction -> Fraction -> Quotient fraction_eq
      intros f1 f2.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2: Fraction
Quotient fraction_eq
      exact (class_of _ (frac_add f1 f2)).
    -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
forall a a' b : Fraction,
fraction_eq a a' ->
((fun f1 f2 : Fraction => class_of fraction_eq (frac_add f1 f2))
 :
 Fraction -> Fraction -> Quotient fraction_eq) a b =
((fun f1 f2 : Fraction => class_of fraction_eq (frac_add f1 f2))
 :
 Fraction -> Fraction -> Quotient fraction_eq) a' b intros f1 f1' f2 p.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f1', f2: Fraction
p: fraction_eq f1 f1'
((fun f0 f3 : Fraction => class_of fraction_eq (frac_add f0 f3))
 :
 Fraction -> Fraction -> Quotient fraction_eq) f1 f2 =
((fun f0 f3 : Fraction => class_of fraction_eq (frac_add f0 f3))
 :
 Fraction -> Fraction -> Quotient fraction_eq) f1' f2  by apply qglue, frac_add_wd_l.
    -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
forall a b b' : Fraction,
fraction_eq b b' ->
((fun f1 f2 : Fraction => class_of fraction_eq (frac_add f1 f2))
 :
 Fraction -> Fraction -> Quotient fraction_eq) a b =
((fun f1 f2 : Fraction => class_of fraction_eq (frac_add f1 f2))
 :
 Fraction -> Fraction -> Quotient fraction_eq) a b' intros f1 f2 f2' q.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2, f2': Fraction
q: fraction_eq f2 f2'
((fun f0 f3 : Fraction => class_of fraction_eq (frac_add f0 f3))
 :
 Fraction -> Fraction -> Quotient fraction_eq) f1 f2 =
((fun f0 f3 : Fraction => class_of fraction_eq (frac_add f0 f3))
 :
 Fraction -> Fraction -> Quotient fraction_eq) f1 f2'  by apply qglue, frac_add_wd_r.
  Defined.

  (** *** Multiplication operation *)

  Definition frac_mult : Fraction -> Fraction -> Fraction :=
    fun '(Build_Fraction n1 d1 p1) '(Build_Fraction n2 d2 p2)
      => Build_Fraction (n1 * n2) (d1 * d2) (mss_mult p1 p2).

  Definition frac_mult_wd_l f1 f1' f2 (p : fraction_eq f1 f1')
    : fraction_eq (frac_mult f1 f2) (frac_mult f1' f2).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f1', f2: Fraction
p: fraction_eq f1 f1'
fraction_eq (frac_mult f1 f2) (frac_mult f1' f2)
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f1', f2: Fraction
p: fraction_eq f1 f1'
fraction_eq (frac_mult f1 f2) (frac_mult f1' f2)
    destruct p as [x [s p]].
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f1', f2: Fraction
x: R
s: S x
p: x * numerator f1 * denominator f1' = x * numerator f1' * denominator f1
fraction_eq (frac_mult f1 f2) (frac_mult f1' f2)
    refine (x; (s, _)); simpl.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f1', f2: Fraction
x: R
s: S x
p: x * numerator f1 * denominator f1' = x * numerator f1' * denominator f1
x * (numerator f1 * numerator f2) * (denominator f1' * denominator f2) =
x * (numerator f1' * numerator f2) * (denominator f1 * denominator f2)
    rewrite 4 rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f1', f2: Fraction
x: R
s: S x
p: x * numerator f1 * denominator f1' = x * numerator f1' * denominator f1
x * numerator f1 * numerator f2 * denominator f1' * denominator f2 =
x * numerator f1' * numerator f2 * denominator f1 * denominator f2
    rewrite (rng_mult_permute_2_3 _ _ (denominator f1')).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f1', f2: Fraction
x: R
s: S x
p: x * numerator f1 * denominator f1' = x * numerator f1' * denominator f1
x * numerator f1 * denominator f1' * numerator f2 * denominator f2 =
x * numerator f1' * numerator f2 * denominator f1 * denominator f2
    rewrite (rng_mult_permute_2_3 _ _ (denominator f1)).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f1', f2: Fraction
x: R
s: S x
p: x * numerator f1 * denominator f1' = x * numerator f1' * denominator f1
x * numerator f1 * denominator f1' * numerator f2 * denominator f2 =
x * numerator f1' * denominator f1 * numerator f2 * denominator f2
    lhs_V napply rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f1', f2: Fraction
x: R
s: S x
p: x * numerator f1 * denominator f1' = x * numerator f1' * denominator f1
x * numerator f1 * denominator f1' * (numerator f2 * denominator f2) =
x * numerator f1' * denominator f1 * numerator f2 * denominator f2
    rhs_V napply rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f1', f2: Fraction
x: R
s: S x
p: x * numerator f1 * denominator f1' = x * numerator f1' * denominator f1
x * numerator f1 * denominator f1' * (numerator f2 * denominator f2) =
x * numerator f1' * denominator f1 * (numerator f2 * denominator f2)
    f_ap.
  Defined.

  Definition frac_mult_wd_r f1 f2 f2' (p : fraction_eq f2 f2')
    : fraction_eq (frac_mult f1 f2) (frac_mult f1 f2').
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2, f2': Fraction
p: fraction_eq f2 f2'
fraction_eq (frac_mult f1 f2) (frac_mult f1 f2')
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2, f2': Fraction
p: fraction_eq f2 f2'
fraction_eq (frac_mult f1 f2) (frac_mult f1 f2')
    destruct p as [x [s p]].
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2, f2': Fraction
x: R
s: S x
p: x * numerator f2 * denominator f2' = x * numerator f2' * denominator f2
fraction_eq (frac_mult f1 f2) (frac_mult f1 f2')
    refine (x; (s, _)); simpl.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2, f2': Fraction
x: R
s: S x
p: x * numerator f2 * denominator f2' = x * numerator f2' * denominator f2
x * (numerator f1 * numerator f2) * (denominator f1 * denominator f2') =
x * (numerator f1 * numerator f2') * (denominator f1 * denominator f2)
    rewrite 4 rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2, f2': Fraction
x: R
s: S x
p: x * numerator f2 * denominator f2' = x * numerator f2' * denominator f2
x * numerator f1 * numerator f2 * denominator f1 * denominator f2' =
x * numerator f1 * numerator f2' * denominator f1 * denominator f2
    rewrite (rng_mult_permute_2_3 _ _ (numerator f2)).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2, f2': Fraction
x: R
s: S x
p: x * numerator f2 * denominator f2' = x * numerator f2' * denominator f2
x * numerator f2 * numerator f1 * denominator f1 * denominator f2' =
x * numerator f1 * numerator f2' * denominator f1 * denominator f2
    rewrite 2 (rng_mult_permute_2_3 _ _ (denominator f2')).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2, f2': Fraction
x: R
s: S x
p: x * numerator f2 * denominator f2' = x * numerator f2' * denominator f2
x * numerator f2 * denominator f2' * numerator f1 * denominator f1 =
x * numerator f1 * numerator f2' * denominator f1 * denominator f2
    rewrite (rng_mult_permute_2_3 _ _ (numerator f2')).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2, f2': Fraction
x: R
s: S x
p: x * numerator f2 * denominator f2' = x * numerator f2' * denominator f2
x * numerator f2 * denominator f2' * numerator f1 * denominator f1 =
x * numerator f2' * numerator f1 * denominator f1 * denominator f2
    rewrite 2 (rng_mult_permute_2_3 _ _ (denominator f2)).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2, f2': Fraction
x: R
s: S x
p: x * numerator f2 * denominator f2' = x * numerator f2' * denominator f2
x * numerator f2 * denominator f2' * numerator f1 * denominator f1 =
x * numerator f2' * denominator f2 * numerator f1 * denominator f1
    lhs_V napply rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2, f2': Fraction
x: R
s: S x
p: x * numerator f2 * denominator f2' = x * numerator f2' * denominator f2
x * numerator f2 * denominator f2' * (numerator f1 * denominator f1) =
x * numerator f2' * denominator f2 * numerator f1 * denominator f1
    rhs_V napply rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2, f2': Fraction
x: R
s: S x
p: x * numerator f2 * denominator f2' = x * numerator f2' * denominator f2
x * numerator f2 * denominator f2' * (numerator f1 * denominator f1) =
x * numerator f2' * denominator f2 * (numerator f1 * denominator f1)
    f_ap.
  Defined.

  Instance mult_rng_localization: Mult (Quotient fraction_eq).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Mult (Quotient fraction_eq)
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Mult (Quotient fraction_eq)
    srapply Quotient_rec2.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Fraction -> Fraction -> Quotient fraction_eq
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
forall a a' b : Fraction, fraction_eq a a' -> ?dclass a b = ?dclass a' b
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
forall a b b' : Fraction, fraction_eq b b' -> ?dclass a b = ?dclass a b'
    -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Fraction -> Fraction -> Quotient fraction_eq cbn.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Fraction -> Fraction -> Quotient fraction_eq
      intros f1 f2.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2: Fraction
Quotient fraction_eq
      exact (class_of _ (frac_mult f1 f2)).
    -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
forall a a' b : Fraction,
fraction_eq a a' ->
((fun f1 f2 : Fraction => class_of fraction_eq (frac_mult f1 f2))
 :
 Fraction -> Fraction -> Quotient fraction_eq) a b =
((fun f1 f2 : Fraction => class_of fraction_eq (frac_mult f1 f2))
 :
 Fraction -> Fraction -> Quotient fraction_eq) a' b intros f1 f1' f2 p; cbn beta.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f1', f2: Fraction
p: fraction_eq f1 f1'
class_of fraction_eq (frac_mult f1 f2) =
class_of fraction_eq (frac_mult f1' f2)
      by apply qglue, frac_mult_wd_l.
    -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
forall a b b' : Fraction,
fraction_eq b b' ->
((fun f1 f2 : Fraction => class_of fraction_eq (frac_mult f1 f2))
 :
 Fraction -> Fraction -> Quotient fraction_eq) a b =
((fun f1 f2 : Fraction => class_of fraction_eq (frac_mult f1 f2))
 :
 Fraction -> Fraction -> Quotient fraction_eq) a b' intros f1 f2 f2' q; cbn beta.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2, f2': Fraction
q: fraction_eq f2 f2'
class_of fraction_eq (frac_mult f1 f2) =
class_of fraction_eq (frac_mult f1 f2')
      by apply qglue, frac_mult_wd_r.
  Defined.

  (** *** Zero element *)

  Instance zero_rng_localization : Zero (Quotient fraction_eq)
    := class_of _ (Build_Fraction 0 1 mss_one).

  (** *** One element *)

  Instance one_rng_localization : One (Quotient fraction_eq)
    := class_of _(Build_Fraction 1 1 mss_one).

  (** *** Negation operation *)

  Definition frac_negate : Fraction -> Fraction
    :=  fun '(Build_Fraction n d p) => Build_Fraction (- n) d p.

  Definition frac_negate_wd f1 f2 (p : fraction_eq f1 f2)
    : fraction_eq (frac_negate f1) (frac_negate f2).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2: Fraction
p: fraction_eq f1 f2
fraction_eq (frac_negate f1) (frac_negate f2)
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2: Fraction
p: fraction_eq f1 f2
fraction_eq (frac_negate f1) (frac_negate f2)
    destruct p as [x [s p]].
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2: Fraction
x: R
s: S x
p: x * numerator f1 * denominator f2 = x * numerator f2 * denominator f1
fraction_eq (frac_negate f1) (frac_negate f2)
    refine (x; (s,_)); simpl.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2: Fraction
x: R
s: S x
p: x * numerator f1 * denominator f2 = x * numerator f2 * denominator f1
x * - numerator f1 * denominator f2 = x * - numerator f2 * denominator f1
    rewrite 2 rng_mult_negate_r, 2 rng_mult_negate_l.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2: Fraction
x: R
s: S x
p: x * numerator f1 * denominator f2 = x * numerator f2 * denominator f1
- (x * numerator f1 * denominator f2) = - (x * numerator f2 * denominator f1)
    f_ap.
  Defined.

  Instance negate_rng_localization : Negate (Quotient fraction_eq).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Negate (Quotient fraction_eq)
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Negate (Quotient fraction_eq)
    srapply Quotient_rec.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Fraction -> Quotient fraction_eq
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
forall a b : Fraction, fraction_eq a b -> ?pclass a = ?pclass b
    -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Fraction -> Quotient fraction_eq intros f.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
Quotient fraction_eq
      apply class_of.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
Fraction
      exact (frac_negate f).
    -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
forall a b : Fraction,
fraction_eq a b ->
(fun f : Fraction => class_of fraction_eq (frac_negate f)) a =
(fun f : Fraction => class_of fraction_eq (frac_negate f)) b intros f1 f2 p.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f1, f2: Fraction
p: fraction_eq f1 f2
(fun f : Fraction => class_of fraction_eq (frac_negate f)) f1 =
(fun f : Fraction => class_of fraction_eq (frac_negate f)) f2
      by apply qglue, frac_negate_wd.
  Defined.

  (** *** Ring laws *)
  
  (** Commutativity of addition *)
  Instance commutative_plus_rng_localization
    : Commutative plus_rng_localization.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Commutative plus_rng_localization
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Commutative plus_rng_localization
    srapply Quotient_ind2_hprop; intros x y.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y: Fraction
(fun x0 y0 : Quotient fraction_eq =>
 plus_rng_localization x0 y0 = plus_rng_localization y0 x0)
  (class_of fraction_eq x) (class_of fraction_eq y)
    apply qglue, fraction_eq_simple; simpl.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y: Fraction
(numerator x * denominator y + numerator y * denominator x) *
(denominator y * denominator x) =
(numerator y * denominator x + numerator x * denominator y) *
(denominator x * denominator y)
    rewrite (rng_mult_comm (denominator y) (denominator x)).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y: Fraction
(numerator x * denominator y + numerator y * denominator x) *
(denominator x * denominator y) =
(numerator y * denominator x + numerator x * denominator y) *
(denominator x * denominator y)
    f_ap; apply rng_plus_comm.
  Defined.

  (** Left additive identity *)
  Instance leftidentity_plus_rng_localization
    : LeftIdentity plus_rng_localization zero_rng_localization.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
LeftIdentity plus_rng_localization zero_rng_localization
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
LeftIdentity plus_rng_localization zero_rng_localization
    srapply Quotient_ind_hprop; intros f.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
(fun x : Quotient fraction_eq =>
 plus_rng_localization zero_rng_localization x = x) 
  (class_of fraction_eq f)
    apply qglue, fraction_eq_simple; simpl.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
(0 * denominator f + numerator f * 1) * denominator f =
numerator f * (1 * denominator f)
    f_ap.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
0 * denominator f + numerator f * 1 = numerator f
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
denominator f = 1 * denominator f
    -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
0 * denominator f + numerator f * 1 = numerator f rewrite rng_mult_zero_l.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
0 + numerator f * 1 = numerator f
      rewrite rng_plus_zero_l.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
numerator f * 1 = numerator f
      apply rng_mult_one_r.
    -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
denominator f = 1 * denominator f symmetry.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
1 * denominator f = denominator f
      apply rng_mult_one_l.
  Defined.

  Instance leftinverse_plus_rng_localization
    : LeftInverse plus_rng_localization negate_rng_localization zero_rng_localization.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
LeftInverse plus_rng_localization negate_rng_localization
  zero_rng_localization
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
LeftInverse plus_rng_localization negate_rng_localization
  zero_rng_localization
    srapply Quotient_ind_hprop; intros f.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
(fun x : Quotient fraction_eq =>
 plus_rng_localization (negate_rng_localization x) x = zero_rng_localization)
  (class_of fraction_eq f)
    apply qglue, fraction_eq_simple; simpl.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
(- numerator f * denominator f + numerator f * denominator f) * 1 =
0 * (denominator f * denominator f)
    refine (rng_mult_one_r _ @ _).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
- numerator f * denominator f + numerator f * denominator f =
0 * (denominator f * denominator f)
    refine (_ @ (rng_mult_zero_l _)^).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
- numerator f * denominator f + numerator f * denominator f = 0
    rewrite rng_mult_negate_l.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
- (numerator f * denominator f) + numerator f * denominator f = 0
    apply rng_plus_negate_l.
  Defined.

  Instance associative_plus_rng_localization
    : Associative plus_rng_localization.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Associative plus_rng_localization
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Associative plus_rng_localization
    srapply Quotient_ind3_hprop; intros x y z.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
(fun x0 y0 z0 : Quotient fraction_eq =>
 plus_rng_localization x0 (plus_rng_localization y0 z0) =
 plus_rng_localization (plus_rng_localization x0 y0) z0)
  (class_of fraction_eq x) (class_of fraction_eq y) 
  (class_of fraction_eq z)
    apply qglue, fraction_eq_simple.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
numerator (frac_add x (frac_add y z)) *
denominator (frac_add (frac_add x y) z) =
numerator (frac_add (frac_add x y) z) *
denominator (frac_add x (frac_add y z))
    simpl.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
(numerator x * (denominator y * denominator z) +
 (numerator y * denominator z + numerator z * denominator y) * denominator x) *
(denominator x * denominator y * denominator z) =
((numerator x * denominator y + numerator y * denominator x) * denominator z +
 numerator z * (denominator x * denominator y)) *
(denominator x * (denominator y * denominator z))
    rewrite ? rng_dist_r.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
numerator x * (denominator y * denominator z) *
(denominator x * denominator y * denominator z) +
(numerator y * denominator z * denominator x *
 (denominator x * denominator y * denominator z) +
 numerator z * denominator y * denominator x *
 (denominator x * denominator y * denominator z)) =
numerator x * denominator y * denominator z *
(denominator x * (denominator y * denominator z)) +
numerator y * denominator x * denominator z *
(denominator x * (denominator y * denominator z)) +
numerator z * (denominator x * denominator y) *
(denominator x * (denominator y * denominator z))
    rewrite ? rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
numerator x * denominator y * denominator z * denominator x * denominator y *
denominator z +
(numerator y * denominator z * denominator x * denominator x * denominator y *
 denominator z +
 numerator z * denominator y * denominator x * denominator x * denominator y *
 denominator z) =
numerator x * denominator y * denominator z * denominator x * denominator y *
denominator z +
numerator y * denominator x * denominator z * denominator x * denominator y *
denominator z +
numerator z * denominator x * denominator y * denominator x * denominator y *
denominator z
    rewrite ? rng_plus_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
numerator x * denominator y * denominator z * denominator x * denominator y *
denominator z +
numerator y * denominator z * denominator x * denominator x * denominator y *
denominator z +
numerator z * denominator y * denominator x * denominator x * denominator y *
denominator z =
numerator x * denominator y * denominator z * denominator x * denominator y *
denominator z +
numerator y * denominator x * denominator z * denominator x * denominator y *
denominator z +
numerator z * denominator x * denominator y * denominator x * denominator y *
denominator z
    do 4 f_ap.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
numerator y * denominator z * denominator x * denominator x =
numerator y * denominator x * denominator z * denominator x
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
numerator z * denominator y * denominator x =
numerator z * denominator x * denominator y
    all: rewrite <- ? rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
numerator y * (denominator z * (denominator x * denominator x)) =
numerator y * (denominator x * (denominator z * denominator x))
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
numerator z * (denominator y * denominator x) =
numerator z * (denominator x * denominator y)
    all: f_ap.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
denominator z * (denominator x * denominator x) =
denominator x * (denominator z * denominator x)
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
denominator y * denominator x = denominator x * denominator y
    2: apply rng_mult_comm.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
denominator z * (denominator x * denominator x) =
denominator x * (denominator z * denominator x)
    rewrite rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
denominator z * denominator x * denominator x =
denominator x * (denominator z * denominator x)
    apply rng_mult_comm.
  Defined.

  Instance leftidentity_mult_rng_localization
    : LeftIdentity mult_rng_localization one_rng_localization.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
LeftIdentity mult_rng_localization one_rng_localization
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
LeftIdentity mult_rng_localization one_rng_localization
    srapply Quotient_ind_hprop; intros f.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
(fun x : Quotient fraction_eq =>
 mult_rng_localization one_rng_localization x = x) 
  (class_of fraction_eq f)
    apply qglue, fraction_eq_simple; simpl.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
1 * numerator f * denominator f = numerator f * (1 * denominator f)
    f_ap; [|symmetry]; apply rng_mult_one_l.
  Defined.

  Instance associative_mult_rng_localization
    : Associative mult_rng_localization.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Associative mult_rng_localization
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Associative mult_rng_localization
    srapply Quotient_ind3_hprop; intros x y z.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
(fun x0 y0 z0 : Quotient fraction_eq =>
 mult_rng_localization x0 (mult_rng_localization y0 z0) =
 mult_rng_localization (mult_rng_localization x0 y0) z0)
  (class_of fraction_eq x) (class_of fraction_eq y) 
  (class_of fraction_eq z)
    apply qglue, fraction_eq_simple.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
numerator (frac_mult x (frac_mult y z)) *
denominator (frac_mult (frac_mult x y) z) =
numerator (frac_mult (frac_mult x y) z) *
denominator (frac_mult x (frac_mult y z))
    f_ap; [|symmetry]; apply rng_mult_assoc.
  Defined.

  Instance commutative_mult_rng_localization
    : Commutative mult_rng_localization.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Commutative mult_rng_localization
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Commutative mult_rng_localization
    srapply Quotient_ind2_hprop; intros x y.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y: Fraction
(fun x0 y0 : Quotient fraction_eq =>
 mult_rng_localization x0 y0 = mult_rng_localization y0 x0)
  (class_of fraction_eq x) (class_of fraction_eq y)
    apply qglue, fraction_eq_simple; simpl.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y: Fraction
numerator x * numerator y * (denominator y * denominator x) =
numerator y * numerator x * (denominator x * denominator y)
    f_ap; rapply rng_mult_comm.
  Defined.

  Instance leftdistribute_rng_localization
    : LeftDistribute mult_rng_localization plus_rng_localization.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
LeftDistribute mult_rng_localization plus_rng_localization
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
LeftDistribute mult_rng_localization plus_rng_localization
    srapply Quotient_ind3_hprop; intros x y z.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
(fun x0 y0 z0 : Quotient fraction_eq =>
 mult_rng_localization x0 (plus_rng_localization y0 z0) =
 plus_rng_localization (mult_rng_localization x0 y0)
   (mult_rng_localization x0 z0))
  (class_of fraction_eq x) (class_of fraction_eq y) 
  (class_of fraction_eq z)
    apply qglue, fraction_eq_simple.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
numerator (frac_mult x (frac_add y z)) *
denominator (frac_add (frac_mult x y) (frac_mult x z)) =
numerator (frac_add (frac_mult x y) (frac_mult x z)) *
denominator (frac_mult x (frac_add y z))
    simpl.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
numerator x * (numerator y * denominator z + numerator z * denominator y) *
(denominator x * denominator y * (denominator x * denominator z)) =
(numerator x * numerator y * (denominator x * denominator z) +
 numerator x * numerator z * (denominator x * denominator y)) *
(denominator x * (denominator y * denominator z))
    rewrite ? rng_dist_l, ? rng_dist_r.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
numerator x * (numerator y * denominator z) *
(denominator x * denominator y * (denominator x * denominator z)) +
numerator x * (numerator z * denominator y) *
(denominator x * denominator y * (denominator x * denominator z)) =
numerator x * numerator y * (denominator x * denominator z) *
(denominator x * (denominator y * denominator z)) +
numerator x * numerator z * (denominator x * denominator y) *
(denominator x * (denominator y * denominator z))
    rewrite ? rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
numerator x * numerator y * denominator z * denominator x * denominator y *
denominator x * denominator z +
numerator x * numerator z * denominator y * denominator x * denominator y *
denominator x * denominator z =
numerator x * numerator y * denominator x * denominator z * denominator x *
denominator y * denominator z +
numerator x * numerator z * denominator x * denominator y * denominator x *
denominator y * denominator z
    do 2 f_ap.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
numerator x * numerator y * denominator z * denominator x * denominator y *
denominator x =
numerator x * numerator y * denominator x * denominator z * denominator x *
denominator y
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
numerator x * numerator z * denominator y * denominator x * denominator y *
denominator x =
numerator x * numerator z * denominator x * denominator y * denominator x *
denominator y
    all: rewrite <- ? rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
numerator x *
(numerator y *
 (denominator z * (denominator x * (denominator y * denominator x)))) =
numerator x *
(numerator y *
 (denominator x * (denominator z * (denominator x * denominator y))))
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
numerator x *
(numerator z *
 (denominator y * (denominator x * (denominator y * denominator x)))) =
numerator x *
(numerator z *
 (denominator x * (denominator y * (denominator x * denominator y))))
    all: do 2 f_ap.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
denominator z * (denominator x * (denominator y * denominator x)) =
denominator x * (denominator z * (denominator x * denominator y))
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
denominator y * (denominator x * (denominator y * denominator x)) =
denominator x * (denominator y * (denominator x * denominator y))
    all: rewrite ? rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
denominator z * denominator x * denominator y * denominator x =
denominator x * denominator z * denominator x * denominator y
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
denominator y * denominator x * denominator y * denominator x =
denominator x * denominator y * denominator x * denominator y
    all: rewrite (rng_mult_comm (_ x)).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
denominator x * denominator z * denominator y * denominator x =
denominator x * denominator z * denominator x * denominator y
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
denominator x * denominator y * denominator y * denominator x =
denominator x * denominator y * denominator x * denominator y
    all: rewrite <- ? rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
denominator x * (denominator z * (denominator y * denominator x)) =
denominator x * (denominator z * (denominator x * denominator y))
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
denominator x * (denominator y * (denominator y * denominator x)) =
denominator x * (denominator y * (denominator x * denominator y))
    all: f_ap.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
denominator z * (denominator y * denominator x) =
denominator z * (denominator x * denominator y)
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
denominator y * (denominator y * denominator x) =
denominator y * (denominator x * denominator y)
    all: rewrite (rng_mult_comm _ (_ y)).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
denominator z * (denominator x * denominator y) =
denominator z * (denominator x * denominator y)
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
denominator y * (denominator x * denominator y) =
denominator y * (denominator x * denominator y)
    all: rewrite <- ? rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
denominator z * (denominator x * denominator y) =
denominator z * (denominator x * denominator y)
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y, z: Fraction
denominator y * (denominator x * denominator y) =
denominator y * (denominator x * denominator y)
    all: f_ap.
  Defined.

  Definition rng_localization : CRing.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
CRing
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
CRing
    snapply Build_CRing'.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
AbGroup
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
One ?R
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Mult ?R
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Commutative mult
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Associative mult
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
LeftDistribute mult plus
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
LeftIdentity mult 1
    (* All of the laws can be found by typeclass search, but it's slightly faster if we fill them in: *)
    1: exact (Build_AbGroup' (Quotient fraction_eq)
                commutative_plus_rng_localization
                associative_plus_rng_localization
                leftidentity_plus_rng_localization
                leftinverse_plus_rng_localization).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
One
  (Build_AbGroup' (Quotient fraction_eq) commutative_plus_rng_localization
     associative_plus_rng_localization leftidentity_plus_rng_localization
     leftinverse_plus_rng_localization)
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Mult
  (Build_AbGroup' (Quotient fraction_eq) commutative_plus_rng_localization
     associative_plus_rng_localization leftidentity_plus_rng_localization
     leftinverse_plus_rng_localization)
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Commutative mult
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
Associative mult
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
LeftDistribute mult plus
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
LeftIdentity mult 1
    all: exact _.
  Defined.

  Definition loc_in : R $-> rng_localization.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
R $-> rng_localization
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
R $-> rng_localization
    snapply Build_RingHomomorphism.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
R -> rng_localization
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
IsSemiRingPreserving ?rng_homo_map
    1: exact (class_of _ o frac_in).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
IsSemiRingPreserving (class_of fraction_eq o frac_in)
    snapply Build_IsSemiRingPreserving.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
IsMonoidPreserving (fun x : R => class_of fraction_eq (frac_in x))
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
IsMonoidPreserving (fun x : R => class_of fraction_eq (frac_in x))
    -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
IsMonoidPreserving (fun x : R => class_of fraction_eq (frac_in x)) snapply Build_IsMonoidPreserving.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
IsSemiGroupPreserving (fun x : R => class_of fraction_eq (frac_in x))
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
IsUnitPreserving (fun x : R => class_of fraction_eq (frac_in x))
      +
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
IsSemiGroupPreserving (fun x : R => class_of fraction_eq (frac_in x)) intros x y.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y: R
class_of fraction_eq (frac_in (sg_op x y)) =
sg_op (class_of fraction_eq (frac_in x)) (class_of fraction_eq (frac_in y))
        snapply qglue.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y: R
fraction_eq (frac_in (sg_op x y)) (frac_add (frac_in x) (frac_in y))
        apply fraction_eq_simple.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y: R
numerator (frac_in (sg_op x y)) *
denominator (frac_add (frac_in x) (frac_in y)) =
numerator (frac_add (frac_in x) (frac_in y)) *
denominator (frac_in (sg_op x y))
        by simpl; rewrite 5 rng_mult_one_r.
      +
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
IsUnitPreserving (fun x : R => class_of fraction_eq (frac_in x)) reflexivity.
    -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
IsMonoidPreserving (fun x : R => class_of fraction_eq (frac_in x)) snapply Build_IsMonoidPreserving.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
IsSemiGroupPreserving (fun x : R => class_of fraction_eq (frac_in x))
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
IsUnitPreserving (fun x : R => class_of fraction_eq (frac_in x))
      +
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
IsSemiGroupPreserving (fun x : R => class_of fraction_eq (frac_in x)) intros x y.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y: R
class_of fraction_eq (frac_in (sg_op x y)) =
sg_op (class_of fraction_eq (frac_in x)) (class_of fraction_eq (frac_in y))
        snapply qglue.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y: R
fraction_eq (frac_in (sg_op x y)) (frac_mult (frac_in x) (frac_in y))
        apply fraction_eq_simple.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x, y: R
numerator (frac_in (sg_op x y)) *
denominator (frac_mult (frac_in x) (frac_in y)) =
numerator (frac_mult (frac_in x) (frac_in y)) *
denominator (frac_in (sg_op x y))
        by simpl; rewrite 3 rng_mult_one_r.
      +
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
IsUnitPreserving (fun x : R => class_of fraction_eq (frac_in x)) reflexivity.
  Defined.
  
  Section Rec.

    Context (T : CRing) (f : R $-> T)
      (H : forall x, S x -> IsInvertible T (f x)).

    Definition rng_localization_rec_map : rng_localization -> T.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
rng_localization -> T
    Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
rng_localization -> T
      srapply Quotient_rec.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
Fraction -> T
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
forall a b : Fraction, fraction_eq a b -> ?pclass a = ?pclass b
      -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
Fraction -> T intros [n d sd].
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
n, d: R
sd: S d
T
        refine (f n * inverse_elem (f d)).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
n, d: R
sd: S d
IsInvertible T (f d)
        exact (H d sd).
      -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
forall a b : Fraction,
fraction_eq a b ->
(fun X : Fraction =>
 (fun (n d : R) (sd : S d) => f n * inverse_elem (f d)) 
   (numerator X) (denominator X) (in_mult_subset_denominator X))
  a =
(fun X : Fraction =>
 (fun (n d : R) (sd : S d) => f n * inverse_elem (f d)) 
   (numerator X) (denominator X) (in_mult_subset_denominator X))
  b simpl.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
forall a b : Fraction,
fraction_eq a b ->
f (numerator a) * inverse_elem (f (denominator a)) =
f (numerator b) * inverse_elem (f (denominator b))
        intros x y z.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
z: fraction_eq x y
f (numerator x) * inverse_elem (f (denominator x)) =
f (numerator y) * inverse_elem (f (denominator y))
        apply rng_inv_moveR_rV.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
z: fraction_eq x y
f (numerator x) =
f (numerator y) * inverse_elem (f (denominator y)) * f (denominator x)
        rhs_V napply rng_mult_move_left_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
z: fraction_eq x y
f (numerator x) =
inverse_elem (f (denominator y)) * f (numerator y) * f (denominator x)
        rhs_V napply rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
z: fraction_eq x y
f (numerator x) =
inverse_elem (f (denominator y)) * (f (numerator y) * f (denominator x))
        apply rng_inv_moveL_Vr.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
z: fraction_eq x y
f (denominator y) * f (numerator x) = f (numerator y) * f (denominator x)
        lhs_V napply rng_homo_mult.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
z: fraction_eq x y
f (denominator y * numerator x) = f (numerator y) * f (denominator x)
        rhs_V napply rng_homo_mult.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
z: fraction_eq x y
f (denominator y * numerator x) = f (numerator y * denominator x)
        napply (equiv_inj (f z.1 *.)).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
z: fraction_eq x y
IsEquiv (mult (f z.1))
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
z: fraction_eq x y
f z.1 * f (denominator y * numerator x) =
f z.1 * f (numerator y * denominator x)
        {
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
z: fraction_eq x y
IsEquiv (mult (f z.1)) napply isequiv_rng_inv_mult_l.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
z: fraction_eq x y
IsInvertible T (f z.1)
          exact (H _ (fst z.2)). }
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
z: fraction_eq x y
f z.1 * f (denominator y * numerator x) =
f z.1 * f (numerator y * denominator x)
        lhs_V napply rng_homo_mult.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
z: fraction_eq x y
f (z.1 * (denominator y * numerator x)) =
f z.1 * f (numerator y * denominator x)
        rhs_V napply rng_homo_mult.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
z: fraction_eq x y
f (z.1 * (denominator y * numerator x)) =
f (z.1 * (numerator y * denominator x))
        lhs napply ap.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
z: fraction_eq x y
z.1 * (denominator y * numerator x) = ?Goal
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
z: fraction_eq x y
f ?Goal = f (z.1 * (numerator y * denominator x))
        1: lhs napply rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
z: fraction_eq x y
z.1 * denominator y * numerator x = ?Goal
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
z: fraction_eq x y
f ?Goal = f (z.1 * (numerator y * denominator x))
        1: napply rng_mult_permute_2_3.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
z: fraction_eq x y
f (z.1 * numerator x * denominator y) =
f (z.1 * (numerator y * denominator x))
        rhs napply ap.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
z: fraction_eq x y
f (z.1 * numerator x * denominator y) = f ?Goal
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
z: fraction_eq x y
z.1 * (numerator y * denominator x) = ?Goal
        2: napply rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
z: fraction_eq x y
f (z.1 * numerator x * denominator y) = f (z.1 * numerator y * denominator x)
        exact (ap f (snd z.2)).
    Defined.

    Instance issemiringpreserving_rng_localization_rec_map
      : IsSemiRingPreserving rng_localization_rec_map.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
IsSemiRingPreserving rng_localization_rec_map
    Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
IsSemiRingPreserving rng_localization_rec_map
      snapply Build_IsSemiRingPreserving.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
IsMonoidPreserving rng_localization_rec_map
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
IsMonoidPreserving rng_localization_rec_map
      -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
IsMonoidPreserving rng_localization_rec_map snapply Build_IsMonoidPreserving.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
IsSemiGroupPreserving rng_localization_rec_map
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
IsUnitPreserving rng_localization_rec_map
        +
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
IsSemiGroupPreserving rng_localization_rec_map srapply Quotient_ind2_hprop.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
forall a b : Fraction,
(fun x y : Quotient fraction_eq =>
 rng_localization_rec_map (sg_op x y) =
 sg_op (rng_localization_rec_map x) (rng_localization_rec_map y))
  (class_of fraction_eq a) (class_of fraction_eq b)
          intros x y; simpl.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (numerator x * denominator y + numerator y * denominator x) *
inverse_elem (f (denominator x * denominator y)) =
sg_op (f (numerator x) * inverse_elem (f (denominator x)))
  (f (numerator y) * inverse_elem (f (denominator y)))
          apply rng_inv_moveR_rV.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (numerator x * denominator y + numerator y * denominator x) =
sg_op (f (numerator x) * inverse_elem (f (denominator x)))
  (f (numerator y) * inverse_elem (f (denominator y))) *
f (denominator x * denominator y)
          rhs napply rng_dist_r.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (numerator x * denominator y + numerator y * denominator x) =
f (numerator x) * inverse_elem (f (denominator x)) *
f (denominator x * denominator y) +
f (numerator y) * inverse_elem (f (denominator y)) *
f (denominator x * denominator y)
          rewrite rng_homo_plus.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (numerator x * denominator y) + f (numerator y * denominator x) =
f (numerator x) * inverse_elem (f (denominator x)) *
f (denominator x * denominator y) +
f (numerator y) * inverse_elem (f (denominator y)) *
f (denominator x * denominator y)
          rewrite 3 rng_homo_mult.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (numerator x) * f (denominator y) + f (numerator y) * f (denominator x) =
f (numerator x) * inverse_elem (f (denominator x)) *
(f (denominator x) * f (denominator y)) +
f (numerator y) * inverse_elem (f (denominator y)) *
(f (denominator x) * f (denominator y))
          f_ap.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (numerator x) * f (denominator y) =
f (numerator x) * inverse_elem (f (denominator x)) *
(f (denominator x) * f (denominator y))
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (numerator y) * f (denominator x) =
f (numerator y) * inverse_elem (f (denominator y)) *
(f (denominator x) * f (denominator y))
          1,2: rhs_V napply rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (numerator x) * f (denominator y) =
f (numerator x) *
(inverse_elem (f (denominator x)) * (f (denominator x) * f (denominator y)))
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (numerator y) * f (denominator x) =
f (numerator y) *
(inverse_elem (f (denominator y)) * (f (denominator x) * f (denominator y)))
          1,2: f_ap.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (denominator y) =
inverse_elem (f (denominator x)) * (f (denominator x) * f (denominator y))
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (denominator x) =
inverse_elem (f (denominator y)) * (f (denominator x) * f (denominator y))
          1,2: lhs_V napply rng_mult_one_l.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
1 * f (denominator y) =
inverse_elem (f (denominator x)) * (f (denominator x) * f (denominator y))
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
1 * f (denominator x) =
inverse_elem (f (denominator y)) * (f (denominator x) * f (denominator y))
          1,2: rhs napply rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
1 * f (denominator y) =
inverse_elem (f (denominator x)) * f (denominator x) * f (denominator y)
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
1 * f (denominator x) =
inverse_elem (f (denominator y)) * f (denominator x) * f (denominator y)
          2: rhs napply rng_mult_comm.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
1 * f (denominator y) =
inverse_elem (f (denominator x)) * f (denominator x) * f (denominator y)
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
1 * f (denominator x) =
f (denominator y) * (inverse_elem (f (denominator y)) * f (denominator x))
          2: rhs napply rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
1 * f (denominator y) =
inverse_elem (f (denominator x)) * f (denominator x) * f (denominator y)
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
1 * f (denominator x) =
f (denominator y) * inverse_elem (f (denominator y)) * f (denominator x)
          1,2: f_ap.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
1 = inverse_elem (f (denominator x)) * f (denominator x)
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
1 = f (denominator y) * inverse_elem (f (denominator y))
          1,2: symmetry.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
inverse_elem (f (denominator x)) * f (denominator x) = 1
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (denominator y) * inverse_elem (f (denominator y)) = 1
          *
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
inverse_elem (f (denominator x)) * f (denominator x) = 1 apply rng_inv_l.
          *
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (denominator y) * inverse_elem (f (denominator y)) = 1 apply rng_inv_r. 
        +
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
IsUnitPreserving rng_localization_rec_map hnf; simpl.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
f 0 * inverse_elem (f 1) = mon_unit rewrite rng_homo_zero.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
0 * inverse_elem (f 1) = mon_unit
          napply rng_mult_zero_l.
      -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
IsMonoidPreserving rng_localization_rec_map snapply Build_IsMonoidPreserving.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
IsSemiGroupPreserving rng_localization_rec_map
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
IsUnitPreserving rng_localization_rec_map
        +
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
IsSemiGroupPreserving rng_localization_rec_map srapply Quotient_ind2_hprop.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
forall a b : Fraction,
(fun x y : Quotient fraction_eq =>
 rng_localization_rec_map (sg_op x y) =
 sg_op (rng_localization_rec_map x) (rng_localization_rec_map y))
  (class_of fraction_eq a) (class_of fraction_eq b)
          intros x y; simpl.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (numerator x * numerator y) *
inverse_elem (f (denominator x * denominator y)) =
sg_op (f (numerator x) * inverse_elem (f (denominator x)))
  (f (numerator y) * inverse_elem (f (denominator y)))
          apply rng_inv_moveR_rV.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (numerator x * numerator y) =
sg_op (f (numerator x) * inverse_elem (f (denominator x)))
  (f (numerator y) * inverse_elem (f (denominator y))) *
f (denominator x * denominator y)
          lhs napply rng_homo_mult.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (numerator x) * f (numerator y) =
sg_op (f (numerator x) * inverse_elem (f (denominator x)))
  (f (numerator y) * inverse_elem (f (denominator y))) *
f (denominator x * denominator y)
          rhs_V napply rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (numerator x) * f (numerator y) =
f (numerator x) * inverse_elem (f (denominator x)) *
(f (numerator y) * inverse_elem (f (denominator y)) *
 f (denominator x * denominator y))
          rhs_V napply rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (numerator x) * f (numerator y) =
f (numerator x) *
(inverse_elem (f (denominator x)) *
 (f (numerator y) * inverse_elem (f (denominator y)) *
  f (denominator x * denominator y)))
          apply ap.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (numerator y) =
inverse_elem (f (denominator x)) *
(f (numerator y) * inverse_elem (f (denominator y)) *
 f (denominator x * denominator y))
          apply rng_inv_moveL_Vr.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (denominator x) * f (numerator y) =
f (numerator y) * inverse_elem (f (denominator y)) *
f (denominator x * denominator y)
          lhs napply rng_mult_comm.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (numerator y) * f (denominator x) =
f (numerator y) * inverse_elem (f (denominator y)) *
f (denominator x * denominator y)
          rhs_V napply rng_mult_assoc.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (numerator y) * f (denominator x) =
f (numerator y) *
(inverse_elem (f (denominator y)) * f (denominator x * denominator y))
          apply ap.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (denominator x) =
inverse_elem (f (denominator y)) * f (denominator x * denominator y)
          apply rng_inv_moveL_Vr.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (denominator y) * f (denominator x) = f (denominator x * denominator y)
          symmetry.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (denominator x * denominator y) = f (denominator y) * f (denominator x)
          rhs napply rng_mult_comm.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x, y: Fraction
f (denominator x * denominator y) = f (denominator x) * f (denominator y)
          napply rng_homo_mult.
        +
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
IsUnitPreserving rng_localization_rec_map apply rng_inv_moveR_rV; symmetry.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
mon_unit * f 1 = f 1
          apply rng_mult_one_l.
    Defined.

    Definition rng_localization_rec : rng_localization $-> T
      := Build_RingHomomorphism rng_localization_rec_map _.
    
    Definition rng_localization_rec_beta
      : rng_localization_rec $o loc_in $== f.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
rng_localization_rec $o loc_in $== f
    Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x : R, S x -> IsInvertible T (f x)
rng_localization_rec $o loc_in $== f
      intros x; simpl.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x: R
f x * inverse_elem (f 1) = f x   
      apply rng_inv_moveR_rV.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x: R
f x = f x * f 1
      lhs_V napply rng_mult_one_r.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x: R
f x * 1 = f x * f 1
      napply ap; symmetry.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f: R $-> T
H: forall x0 : R, S x0 -> IsInvertible T (f x0)
x: R
f 1 = 1
      apply rng_homo_one.
    Defined.
  
  End Rec.
  
  (** Elements belonging to the multiplicative subset [S] of [R] become invertible in [rng_localization R S]. *)
  #[export] Instance isinvertible_rng_localization (x : R) (Sx : S x)
    : IsInvertible rng_localization (loc_in x).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x: R
Sx: S x
IsInvertible rng_localization (loc_in x)
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x: R
Sx: S x
IsInvertible rng_localization (loc_in x)
    snapply isinvertible_cring.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x: R
Sx: S x
rng_localization
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x: R
Sx: S x
?inv * loc_in x = 1
    -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x: R
Sx: S x
rng_localization exact (class_of _ (Build_Fraction 1 x Sx)).
    -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x: R
Sx: S x
class_of fraction_eq
  {| numerator := 1; denominator := x; in_mult_subset_denominator := Sx |} *
loc_in x = 1 apply qglue, fraction_eq_simple.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
x: R
Sx: S x
numerator
  (frac_mult
     {| numerator := 1; denominator := x; in_mult_subset_denominator := Sx |}
     (frac_in x)) *
denominator
  {|
    numerator := 1; denominator := 1; in_mult_subset_denominator := mss_one
  |} =
numerator
  {|
    numerator := 1; denominator := 1; in_mult_subset_denominator := mss_one
  |} *
denominator
  (frac_mult
     {| numerator := 1; denominator := x; in_mult_subset_denominator := Sx |}
     (frac_in x))
      exact (ring_mult_assoc_opp _ _ _ _).
  Defined.
  
  (** As a special case, any denominator of a fraction must necessarily be invertible. *)
  #[export] Instance isinvertible_denominator (f : Fraction)
    : IsInvertible rng_localization (loc_in (denominator f)).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
IsInvertible rng_localization (loc_in (denominator f))
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
IsInvertible rng_localization (loc_in (denominator f))
    snapply isinvertible_rng_localization.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
S (denominator f)
    exact (in_mult_subset_denominator f).
  Defined.
  
  (** Elements that were invertible in the original ring [R], continue to be invertible in [rng_localization R S]. Since [loc_in] is a ring homomorphism this is automatic. *)
  Definition isinvertible_rng_localization_preserved (x : R)
    : IsInvertible R x -> IsInvertible rng_localization (loc_in x)
    := _.
  
  (** We can factor any fraction as the multiplication of the numerator and the inverse of the denominator. *)
  Definition fraction_decompose (f : Fraction)
    : class_of fraction_eq f
      = loc_in (numerator f) * inverse_elem (loc_in (denominator f)).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
class_of fraction_eq f =
loc_in (numerator f) * inverse_elem (loc_in (denominator f))
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
class_of fraction_eq f =
loc_in (numerator f) * inverse_elem (loc_in (denominator f))
    apply qglue, fraction_eq_simple.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
f: Fraction
numerator f *
denominator
  (frac_mult (frac_in (numerator f))
     {|
       numerator := 1;
       denominator := denominator f;
       in_mult_subset_denominator := in_mult_subset_denominator f
     |}) =
numerator
  (frac_mult (frac_in (numerator f))
     {|
       numerator := 1;
       denominator := denominator f;
       in_mult_subset_denominator := in_mult_subset_denominator f
     |}) *
denominator f
    napply rng_mult_assoc.
  Defined.

  Definition rng_localization_ind
    (P : rng_localization -> Type)
    (H : forall x, IsHProp (P x))
    (Hin : forall x, P (loc_in x))
    (Hinv : forall x (H : IsInvertible rng_localization x),
      P x -> P (inverse_elem x))
    (Hmul : forall x y, P x -> P y -> P (x * y))
    : forall x, P x.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
P: rng_localization -> Type
H: forall x : rng_localization, IsHProp (P x)
Hin: forall x : R, P (loc_in x)
Hinv: forall (x : rng_localization) (H0 : IsInvertible rng_localization x),
P x -> P (inverse_elem x)
Hmul: forall x y : rng_localization, P x -> P y -> P (x * y)
forall x : rng_localization, P x
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
P: rng_localization -> Type
H: forall x : rng_localization, IsHProp (P x)
Hin: forall x : R, P (loc_in x)
Hinv: forall (x : rng_localization) (H0 : IsInvertible rng_localization x),
P x -> P (inverse_elem x)
Hmul: forall x y : rng_localization, P x -> P y -> P (x * y)
forall x : rng_localization, P x
    snapply Quotient_ind.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
P: rng_localization -> Type
H: forall x : rng_localization, IsHProp (P x)
Hin: forall x : R, P (loc_in x)
Hinv: forall (x : rng_localization) (H0 : IsInvertible rng_localization x),
P x -> P (inverse_elem x)
Hmul: forall x y : rng_localization, P x -> P y -> P (x * y)
forall x : Quotient fraction_eq, IsHSet (P x)
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
P: rng_localization -> Type
H: forall x : rng_localization, IsHProp (P x)
Hin: forall x : R, P (loc_in x)
Hinv: forall (x : rng_localization) (H0 : IsInvertible rng_localization x),
P x -> P (inverse_elem x)
Hmul: forall x y : rng_localization, P x -> P y -> P (x * y)
forall a : Fraction, P (class_of fraction_eq a)
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
P: rng_localization -> Type
H: forall x : rng_localization, IsHProp (P x)
Hin: forall x : R, P (loc_in x)
Hinv: forall (x : rng_localization) (H0 : IsInvertible rng_localization x),
P x -> P (inverse_elem x)
Hmul: forall x y : rng_localization, P x -> P y -> P (x * y)
forall (a b : Fraction) (H0 : fraction_eq a b),
transport P (qglue H0) (?pclass a) = ?pclass b
    -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
P: rng_localization -> Type
H: forall x : rng_localization, IsHProp (P x)
Hin: forall x : R, P (loc_in x)
Hinv: forall (x : rng_localization) (H0 : IsInvertible rng_localization x),
P x -> P (inverse_elem x)
Hmul: forall x y : rng_localization, P x -> P y -> P (x * y)
forall x : Quotient fraction_eq, IsHSet (P x) exact _.
    -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
P: rng_localization -> Type
H: forall x : rng_localization, IsHProp (P x)
Hin: forall x : R, P (loc_in x)
Hinv: forall (x : rng_localization) (H0 : IsInvertible rng_localization x),
P x -> P (inverse_elem x)
Hmul: forall x y : rng_localization, P x -> P y -> P (x * y)
forall a : Fraction, P (class_of fraction_eq a) intros f.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
P: rng_localization -> Type
H: forall x : rng_localization, IsHProp (P x)
Hin: forall x : R, P (loc_in x)
Hinv: forall (x : rng_localization) (H0 : IsInvertible rng_localization x),
P x -> P (inverse_elem x)
Hmul: forall x y : rng_localization, P x -> P y -> P (x * y)
f: Fraction
P (class_of fraction_eq f)
      refine (transport P (fraction_decompose f)^ _).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
P: rng_localization -> Type
H: forall x : rng_localization, IsHProp (P x)
Hin: forall x : R, P (loc_in x)
Hinv: forall (x : rng_localization) (H0 : IsInvertible rng_localization x),
P x -> P (inverse_elem x)
Hmul: forall x y : rng_localization, P x -> P y -> P (x * y)
f: Fraction
P (loc_in (numerator f) * inverse_elem (loc_in (denominator f)))
      apply Hmul.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
P: rng_localization -> Type
H: forall x : rng_localization, IsHProp (P x)
Hin: forall x : R, P (loc_in x)
Hinv: forall (x : rng_localization) (H0 : IsInvertible rng_localization x),
P x -> P (inverse_elem x)
Hmul: forall x y : rng_localization, P x -> P y -> P (x * y)
f: Fraction
P (loc_in (numerator f))
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
P: rng_localization -> Type
H: forall x : rng_localization, IsHProp (P x)
Hin: forall x : R, P (loc_in x)
Hinv: forall (x : rng_localization) (H0 : IsInvertible rng_localization x),
P x -> P (inverse_elem x)
Hmul: forall x y : rng_localization, P x -> P y -> P (x * y)
f: Fraction
P (inverse_elem (loc_in (denominator f)))
      +
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
P: rng_localization -> Type
H: forall x : rng_localization, IsHProp (P x)
Hin: forall x : R, P (loc_in x)
Hinv: forall (x : rng_localization) (H0 : IsInvertible rng_localization x),
P x -> P (inverse_elem x)
Hmul: forall x y : rng_localization, P x -> P y -> P (x * y)
f: Fraction
P (loc_in (numerator f)) apply Hin.
      +
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
P: rng_localization -> Type
H: forall x : rng_localization, IsHProp (P x)
Hin: forall x : R, P (loc_in x)
Hinv: forall (x : rng_localization) (H0 : IsInvertible rng_localization x),
P x -> P (inverse_elem x)
Hmul: forall x y : rng_localization, P x -> P y -> P (x * y)
f: Fraction
P (inverse_elem (loc_in (denominator f))) apply Hinv, Hin.
    -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
P: rng_localization -> Type
H: forall x : rng_localization, IsHProp (P x)
Hin: forall x : R, P (loc_in x)
Hinv: forall (x : rng_localization) (H0 : IsInvertible rng_localization x),
P x -> P (inverse_elem x)
Hmul: forall x y : rng_localization, P x -> P y -> P (x * y)
forall (a b : Fraction) (H0 : fraction_eq a b),
transport P (qglue H0)
  ((fun f : Fraction =>
    transport P (fraction_decompose f)^
      (Hmul (loc_in (numerator f)) (inverse_elem (loc_in (denominator f)))
         (Hin (numerator f))
         (Hinv (loc_in (denominator f)) (isinvertible_denominator f)
            (Hin (denominator f)))))
     a) =
(fun f : Fraction =>
 transport P (fraction_decompose f)^
   (Hmul (loc_in (numerator f)) (inverse_elem (loc_in (denominator f)))
      (Hin (numerator f))
      (Hinv (loc_in (denominator f)) (isinvertible_denominator f)
         (Hin (denominator f)))))
  b intros f1 f2 p.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
P: rng_localization -> Type
H: forall x : rng_localization, IsHProp (P x)
Hin: forall x : R, P (loc_in x)
Hinv: forall (x : rng_localization) (H0 : IsInvertible rng_localization x),
P x -> P (inverse_elem x)
Hmul: forall x y : rng_localization, P x -> P y -> P (x * y)
f1, f2: Fraction
p: fraction_eq f1 f2
transport P (qglue p)
  ((fun f : Fraction =>
    transport P (fraction_decompose f)^
      (Hmul (loc_in (numerator f)) (inverse_elem (loc_in (denominator f)))
         (Hin (numerator f))
         (Hinv (loc_in (denominator f)) (isinvertible_denominator f)
            (Hin (denominator f)))))
     f1) =
(fun f : Fraction =>
 transport P (fraction_decompose f)^
   (Hmul (loc_in (numerator f)) (inverse_elem (loc_in (denominator f)))
      (Hin (numerator f))
      (Hinv (loc_in (denominator f)) (isinvertible_denominator f)
         (Hin (denominator f)))))
  f2
      apply path_ishprop.
  Defined.
  
  Definition rng_localization_ind_homotopy {T : CRing}
    {f g : rng_localization $-> T}
    (p : f $o loc_in $== g $o loc_in)
    : f $== g.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f, g: rng_localization $-> T
p: f $o loc_in $== g $o loc_in
f $== g
  Proof.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f, g: rng_localization $-> T
p: f $o loc_in $== g $o loc_in
f $== g
    srapply rng_localization_ind.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f, g: rng_localization $-> T
p: f $o loc_in $== g $o loc_in
forall x : R,
(fun x0 : rng_localization =>
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) f x0 =
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) g x0)
  (loc_in x)
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f, g: rng_localization $-> T
p: f $o loc_in $== g $o loc_in
forall (x : rng_localization) (H : IsInvertible rng_localization x),
(fun x0 : rng_localization =>
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) f x0 =
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) g x0) x ->
(fun x0 : rng_localization =>
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) f x0 =
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) g x0)
  (inverse_elem x)
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f, g: rng_localization $-> T
p: f $o loc_in $== g $o loc_in
forall x y : rng_localization,
(fun x0 : rng_localization =>
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) f x0 =
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) g x0) x ->
(fun x0 : rng_localization =>
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) f x0 =
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) g x0) y ->
(fun x0 : rng_localization =>
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) f x0 =
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) g x0)
  (x * y)
    -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f, g: rng_localization $-> T
p: f $o loc_in $== g $o loc_in
forall x : R,
(fun x0 : rng_localization =>
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) f x0 =
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) g x0)
  (loc_in x) exact p.
    -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f, g: rng_localization $-> T
p: f $o loc_in $== g $o loc_in
forall (x : rng_localization) (H : IsInvertible rng_localization x),
(fun x0 : rng_localization =>
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) f x0 =
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) g x0) x ->
(fun x0 : rng_localization =>
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) f x0 =
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) g x0)
  (inverse_elem x) hnf; intros x H q.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f, g: rng_localization $-> T
p: f $o loc_in $== g $o loc_in
x: rng_localization
H: IsInvertible rng_localization x
q: f x = g x
f (inverse_elem x) = g (inverse_elem x)
      change (inverse_elem (f x) = inverse_elem (g x)).
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f, g: rng_localization $-> T
p: f $o loc_in $== g $o loc_in
x: rng_localization
H: IsInvertible rng_localization x
q: f x = g x
inverse_elem (f x) = inverse_elem (g x)
      apply isinvertible_unique.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f, g: rng_localization $-> T
p: f $o loc_in $== g $o loc_in
x: rng_localization
H: IsInvertible rng_localization x
q: f x = g x
f x = g x
      exact q.
    -
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f, g: rng_localization $-> T
p: f $o loc_in $== g $o loc_in
forall x y : rng_localization,
(fun x0 : rng_localization =>
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) f x0 =
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) g x0) x ->
(fun x0 : rng_localization =>
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) f x0 =
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) g x0) y ->
(fun x0 : rng_localization =>
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) f x0 =
 (rng_homo_map rng_localization T
  :
  RingHomomorphism rng_localization T -> rng_localization $-> T) g x0)
  (x * y) hnf; intros x y q r.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f, g: rng_localization $-> T
p: f $o loc_in $== g $o loc_in
x, y: rng_localization
q: f x = g x
r: f y = g y
f (x * y) = g (x * y)
      lhs napply rng_homo_mult.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f, g: rng_localization $-> T
p: f $o loc_in $== g $o loc_in
x, y: rng_localization
q: f x = g x
r: f y = g y
f x * f y = g (x * y)
      rhs napply rng_homo_mult.
R: CRing
S: R -> Type
IsMultiplicativeSubset0: IsMultiplicativeSubset S
T: CRing
f, g: rng_localization $-> T
p: f $o loc_in $== g $o loc_in
x, y: rng_localization
q: f x = g x
r: f y = g y
f x * f y = g x * g y
      f_ap.
  Defined.

End Localization.

(** TODO: Show construction is a localization. *)