rings.v

Require Import
  HoTT.Classes.theory.groups
  HoTT.Classes.theory.apartness.[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Import
  HoTT.Classes.interfaces.abstract_algebra.

Generalizable Variables R A B C f z.

Definition is_ne_0 `(x : R) `{Zero R} `{p : PropHolds (x <> 0)}
  : x <> 0 := p.
Definition is_nonneg `(x : R) `{Le R} `{Zero R} `{p : PropHolds (0 ≤ x)}
  : 0 ≤ x := p.
Definition is_pos `(x : R) `{Lt R} `{Zero R} `{p : PropHolds (0 < x)}
  : 0 < x := p.

(* Lemma stdlib_semiring_theory R `{SemiRing R}
  : Ring_theory.semi_ring_theory 0 1 (+) (.*.) (=).
Proof.
Qed.
*)

(* We cannot apply [left_cancellation (.*.) z] directly in case we have
  no [PropHolds (0 <> z)] instance in the context. *)
Section cancellation.
  Context `(op : A -> A -> A) `{!Zero A}.

  Lemma left_cancellation_ne_0
    `{forall z, PropHolds (z <> 0) -> LeftCancellation op z} z
    : z <> 0 -> LeftCancellation op z.A: Type
op: A -> A -> A
Zero0: Zero A
H: forall z : A,
PropHolds (z <> 0) -> LeftCancellation op z
z: A
z <> 0 -> LeftCancellation op z
  Proof.A: Type
op: A -> A -> A
Zero0: Zero A
H: forall z : A,
PropHolds (z <> 0) -> LeftCancellation op z
z: A
z <> 0 -> LeftCancellation op z auto. Qed.

  Lemma right_cancellation_ne_0
    `{forall z, PropHolds (z <> 0) -> RightCancellation op z} z
    : z <> 0 -> RightCancellation op z.A: Type
op: A -> A -> A
Zero0: Zero A
H: forall z : A,
PropHolds (z <> 0) -> RightCancellation op z
z: A
z <> 0 -> RightCancellation op z
  Proof.A: Type
op: A -> A -> A
Zero0: Zero A
H: forall z : A,
PropHolds (z <> 0) -> RightCancellation op z
z: A
z <> 0 -> RightCancellation op z auto. Qed.

  Lemma right_cancel_from_left `{!Commutative op} `{!LeftCancellation op z}
    : RightCancellation op z.A: Type
op: A -> A -> A
Zero0: Zero A
Commutative0: Commutative op
z: A
LeftCancellation0: LeftCancellation op z
RightCancellation op z
  Proof.A: Type
op: A -> A -> A
Zero0: Zero A
Commutative0: Commutative op
z: A
LeftCancellation0: LeftCancellation op z
RightCancellation op z
  intros x y E.A: Type
op: A -> A -> A
Zero0: Zero A
Commutative0: Commutative op
z: A
LeftCancellation0: LeftCancellation op z
x, y: A
E: op x z = op y z
x = y
  apply (left_cancellation op z).A: Type
op: A -> A -> A
Zero0: Zero A
Commutative0: Commutative op
z: A
LeftCancellation0: LeftCancellation op z
x, y: A
E: op x z = op y z
op z x = op z y
  rewrite 2!(commutativity (f:=op) z _).A: Type
op: A -> A -> A
Zero0: Zero A
Commutative0: Commutative op
z: A
LeftCancellation0: LeftCancellation op z
x, y: A
E: op x z = op y z
op x z = op y z
  assumption.
  Qed.
End cancellation.

Section strong_cancellation.
  Context `{IsApart A} (op : A -> A -> A).

  Lemma strong_right_cancel_from_left `{!Commutative op} 
    `{!StrongLeftCancellation op z}
    : StrongRightCancellation op z.A: Type
Aap: Apart A
H: IsApart A
op: A -> A -> A
Commutative0: Commutative op
z: A
StrongLeftCancellation0: StrongLeftCancellation op z
StrongRightCancellation op z
  Proof.A: Type
Aap: Apart A
H: IsApart A
op: A -> A -> A
Commutative0: Commutative op
z: A
StrongLeftCancellation0: StrongLeftCancellation op z
StrongRightCancellation op z
  intros x y E.A: Type
Aap: Apart A
H: IsApart A
op: A -> A -> A
Commutative0: Commutative op
z: A
StrongLeftCancellation0: StrongLeftCancellation op z
x, y: A
E: x ≶ y
op x z ≶ op y z
  rewrite 2!(commutativity _ z).A: Type
Aap: Apart A
H: IsApart A
op: A -> A -> A
Commutative0: Commutative op
z: A
StrongLeftCancellation0: StrongLeftCancellation op z
x, y: A
E: x ≶ y
op z x ≶ op z y
  apply (strong_left_cancellation op z);trivial.
  Qed.

  Global Instance strong_left_cancellation_cancel `{!StrongLeftCancellation op z}
    : LeftCancellation op z | 20.A: Type
Aap: Apart A
H: IsApart A
op: A -> A -> A
z: A
StrongLeftCancellation0: StrongLeftCancellation op z
LeftCancellation op z
  Proof.A: Type
Aap: Apart A
H: IsApart A
op: A -> A -> A
z: A
StrongLeftCancellation0: StrongLeftCancellation op z
LeftCancellation op z
  intros x y E1.A: Type
Aap: Apart A
H: IsApart A
op: A -> A -> A
z: A
StrongLeftCancellation0: StrongLeftCancellation op z
x, y: A
E1: op z x = op z y
x = y
  apply tight_apart in E1;apply tight_apart;intros E2.A: Type
Aap: Apart A
H: IsApart A
op: A -> A -> A
z: A
StrongLeftCancellation0: StrongLeftCancellation op z
x, y: A
E1: ~ (op z x ≶ op z y)
E2: x ≶ y
Empty
  apply E1.A: Type
Aap: Apart A
H: IsApart A
op: A -> A -> A
z: A
StrongLeftCancellation0: StrongLeftCancellation op z
x, y: A
E1: ~ (op z x ≶ op z y)
E2: x ≶ y
op z x ≶ op z y apply (strong_left_cancellation op);trivial.
  Qed.

  Global Instance strong_right_cancellation_cancel `{!StrongRightCancellation op z}
    : RightCancellation op z | 20.A: Type
Aap: Apart A
H: IsApart A
op: A -> A -> A
z: A
StrongRightCancellation0: StrongRightCancellation op
  z
RightCancellation op z
  Proof.A: Type
Aap: Apart A
H: IsApart A
op: A -> A -> A
z: A
StrongRightCancellation0: StrongRightCancellation op
  z
RightCancellation op z
  intros x y E1.A: Type
Aap: Apart A
H: IsApart A
op: A -> A -> A
z: A
StrongRightCancellation0: StrongRightCancellation op
  z
x, y: A
E1: op x z = op y z
x = y
  apply tight_apart in E1;apply tight_apart;intros E2.A: Type
Aap: Apart A
H: IsApart A
op: A -> A -> A
z: A
StrongRightCancellation0: StrongRightCancellation op
  z
x, y: A
E1: ~ (op x z ≶ op y z)
E2: x ≶ y
Empty
  apply E1.A: Type
Aap: Apart A
H: IsApart A
op: A -> A -> A
z: A
StrongRightCancellation0: StrongRightCancellation op
  z
x, y: A
E1: ~ (op x z ≶ op y z)
E2: x ≶ y
op x z ≶ op y z apply (strong_right_cancellation op);trivial.
  Qed.
End strong_cancellation.

Section semiring_props.
  Context `{IsSemiCRing R}.
(*   Add Ring SR : (stdlib_semiring_theory R). *)

  Instance mult_ne_0 `{!NoZeroDivisors R} x y
    : PropHolds (x <> 0) -> PropHolds (y <> 0) -> PropHolds (x * y <> 0).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
NoZeroDivisors0: NoZeroDivisors R
x, y: R
PropHolds (x <> 0) ->
PropHolds (y <> 0) -> PropHolds (x * y <> 0)
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
NoZeroDivisors0: NoZeroDivisors R
x, y: R
PropHolds (x <> 0) ->
PropHolds (y <> 0) -> PropHolds (x * y <> 0)
  intros Ex Ey Exy.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
NoZeroDivisors0: NoZeroDivisors R
x, y: R
Ex: PropHolds (x <> 0)
Ey: PropHolds (y <> 0)
Exy: x * y = 0
Empty
  unfold PropHolds in *.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
NoZeroDivisors0: NoZeroDivisors R
x, y: R
Ex: x <> 0
Ey: y <> 0
Exy: x * y = 0
Empty
  apply (no_zero_divisors x); split; eauto.
  Qed.

  Global Instance plus_0_r: RightIdentity (+) 0 := right_identity.
  Global Instance plus_0_l: LeftIdentity (+) 0 := left_identity.
  Global Instance mult_1_l: LeftIdentity (.*.) 1 := left_identity.
  Global Instance mult_1_r: RightIdentity (.*.) 1 := right_identity.

  Global Instance plus_assoc: Associative (+) := simple_associativity.
  Global Instance mult_assoc: Associative (.*.) := simple_associativity.

  Global Instance plus_comm: Commutative (+) := commutativity.
  Global Instance mult_comm: Commutative (.*.) := commutativity.

  Global Instance mult_0_l: LeftAbsorb (.*.) 0 := left_absorb.

  Global Instance mult_0_r: RightAbsorb (.*.) 0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
RightAbsorb mult 0
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
RightAbsorb mult 0
  intro.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
x: R
x * 0 = 0 path_via (0 * x).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
x: R
x * 0 = 0 * x
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
x: R
0 * x = 0
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
x: R
x * 0 = 0 * x apply mult_comm.
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
x: R
0 * x = 0 apply left_absorb.
  Qed.

  Global Instance plus_mult_distr_r : RightDistribute (.*.) (+).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
RightDistribute mult plus
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
RightDistribute mult plus
  intros x y z.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
x, y, z: R
(x + y) * z = x * z + y * z
  etransitivity;[|etransitivity].R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
x, y, z: R
(x + y) * z = ?Goal
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
x, y, z: R
?Goal = ?Goal1
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
x, y, z: R
?Goal1 = x * z + y * z
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
x, y, z: R
(x + y) * z = ?Goal apply mult_comm.
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
x, y, z: R
z * (x + y) = ?Goal apply distribute_l.
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
x, y, z: R
z * x + z * y = x * z + y * z apply ap011;apply mult_comm.
  Qed.

  Lemma plus_mult_distr_l : LeftDistribute (.*.) (+).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
LeftDistribute mult plus
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
LeftDistribute mult plus
  apply _.
  Qed.

  Global Instance: forall r : R, @IsMonoidPreserving R R (+) (+) 0 0 (r *.).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
forall r : R, IsMonoidPreserving (mult r)
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
forall r : R, IsMonoidPreserving (mult r)
  repeat (constructor; try apply _).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
r: R
IsSemiGroupPreserving (mult r)
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
r: R
IsUnitPreserving (mult r)
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
r: R
IsSemiGroupPreserving (mult r) red.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
r: R
forall x y : R, r * sg_op x y = sg_op (r * x) (r * y) apply distribute_l.
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
H: IsSemiCRing R
r: R
IsUnitPreserving (mult r) apply right_absorb.
  Qed.
End semiring_props.

(* Due to bug #2528 *)
#[export]
Hint Extern 3 (PropHolds (_ * _ <> 0)) => eapply @mult_ne_0 : typeclass_instances.

Section semiringmor_props.
  Context `{IsSemiRingPreserving A B f}.

  Lemma preserves_0: f 0 = 0.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
f 0 = 0
  Proof.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
f 0 = 0 apply preserves_mon_unit. Qed.
  Lemma preserves_1: f 1 = 1.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
f 1 = 1
  Proof.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
f 1 = 1 apply preserves_mon_unit. Qed.
  Lemma preserves_mult: forall x y, f (x * y) = f x * f y.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
forall x y : A, f (x * y) = f x * f y
  Proof.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
forall x y : A, f (x * y) = f x * f y
  intros.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
x, y: A
f (x * y) = f x * f y apply preserves_sg_op.
  Qed.
  Lemma preserves_plus: forall x y, f (x + y) = f x + f y.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
forall x y : A, f (x + y) = f x + f y
  Proof.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
forall x y : A, f (x + y) = f x + f y
  intros.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
x, y: A
f (x + y) = f x + f y apply preserves_sg_op.
  Qed.

  Lemma preserves_2: f 2 = 2.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
f 2 = 2
  Proof.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
f 2 = 2
  rewrite preserves_plus.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
f 1 + f 1 = 2 rewrite preserves_1.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
2 = 2 reflexivity.
  Qed.

  Lemma preserves_3: f 3 = 3.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
f 3 = 3
  Proof.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
f 3 = 3
  rewrite ?preserves_plus, ?preserves_1.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
3 = 3
  reflexivity.
  Qed.

  Lemma preserves_4: f 4 = 4.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
f 4 = 4
  Proof.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
f 4 = 4
  rewrite ?preserves_plus, ?preserves_1.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
4 = 4
  reflexivity.
  Qed.

  Context `{!IsInjective f}.
  Instance isinjective_ne_0 x : PropHolds (x <> 0) -> PropHolds (f x <> 0).A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
IsInjective0: IsInjective f
x: A
PropHolds (x <> 0) -> PropHolds (f x <> 0)
  Proof.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
IsInjective0: IsInjective f
x: A
PropHolds (x <> 0) -> PropHolds (f x <> 0)
  intros.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
IsInjective0: IsInjective f
x: A
X: PropHolds (x <> 0)
PropHolds (f x <> 0) rewrite <-preserves_0.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
IsInjective0: IsInjective f
x: A
X: PropHolds (x <> 0)
PropHolds (f x <> f 0) apply (isinjective_ne f).A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
IsInjective0: IsInjective f
x: A
X: PropHolds (x <> 0)
x <> 0
  assumption.
  Qed.

  Lemma injective_ne_1 x : x <> 1 -> f x <> 1.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
IsInjective0: IsInjective f
x: A
x <> 1 -> f x <> 1
  Proof.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
IsInjective0: IsInjective f
x: A
x <> 1 -> f x <> 1
  intros.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
IsInjective0: IsInjective f
x: A
X: x <> 1
f x <> 1 rewrite <-preserves_1.A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
IsInjective0: IsInjective f
x: A
X: x <> 1
f x <> f 1
  apply (isinjective_ne f).A, B: Type
Aplus: Plus A
Bplus: Plus B
Amult: Mult A
Bmult: Mult B
Azero: Zero A
Bzero: Zero B
Aone: One A
Bone: One B
f: A -> B
H: IsSemiRingPreserving f
IsInjective0: IsInjective f
x: A
X: x <> 1
x <> 1
  assumption.
  Qed.
End semiringmor_props.

(* Due to bug #2528 *)
#[export]
Hint Extern 12 (PropHolds (_ _ <> 0)) =>
  eapply @isinjective_ne_0 : typeclass_instances.

(* Lemma stdlib_ring_theory R `{Ring R} :
  Ring_theory.ring_theory 0 1 (+) (.*.) (fun x y => x - y) (-) (=).
Proof.
Qed.
*)
Section cring_props.
  Context `{IsCRing R}.

  Instance: LeftAbsorb (.*.) 0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
LeftAbsorb mult 0
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
LeftAbsorb mult 0
  intro.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
y: R
0 * y = 0
  rewrite (commutativity (f:=(.*.)) 0).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
y: R
y * 0 = 0
  apply (left_cancellation (+) (y * 0)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
y: R
y * 0 + y * 0 = y * 0 + 0
  path_via (y * 0);[|apply symmetry, right_identity].R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
y: R
y * 0 + y * 0 = y * 0
  path_via (y * (0 + 0)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
y: R
y * 0 + y * 0 = y * (0 + 0)
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
y: R
y * (0 + 0) = y * 0
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
y: R
y * 0 + y * 0 = y * (0 + 0) apply symmetry,distribute_l.
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
y: R
y * (0 + 0) = y * 0 apply ap.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
y: R
0 + 0 = 0 apply right_identity.
  Qed.

  Global Instance CRing_Semi: IsSemiCRing R.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
IsSemiCRing R
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsCRing R
IsSemiCRing R
  repeat (constructor; try apply _).
  Qed.

End cring_props.


Section ring_props.
  Context `{IsRing R}.

  Global Instance mult_left_absorb : LeftAbsorb (.*.) 0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
LeftAbsorb mult 0
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
LeftAbsorb mult 0
    intro y.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
y: R
0 * y = 0
    rapply (right_cancellation (+) (0 * y)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
y: R
0 * y + 0 * y = 0 + 0 * y
    lhs_V rapply simple_distribute_r.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
y: R
(0 + 0) * y = 0 + 0 * y
    rhs rapply left_identity.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
y: R
(0 + 0) * y = 0 * y
    nrapply (ap (.* y)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
y: R
0 + 0 = 0
    apply left_identity.
  Defined.

  Global Instance mult_right_absorb : RightAbsorb (.*.) 0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
RightAbsorb mult 0
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
RightAbsorb mult 0
    intro x.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
x * 0 = 0
    rapply (right_cancellation (+) (x * 0)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
x * 0 + x * 0 = 0 + x * 0
    lhs_V rapply simple_distribute_l.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
x * (0 + 0) = 0 + x * 0
    rhs rapply left_identity.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
x * (0 + 0) = x * 0
    nrapply (ap (x *.)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
0 + 0 = 0
    apply left_identity.
  Defined.

  Definition negate_involutive x : - - x = x := groups.negate_involutive x.
  (* alias for convenience *)

  Lemma plus_negate_r : forall x, x + -x = 0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
forall x : R, x - x = 0
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
forall x : R, x - x = 0 exact right_inverse. Qed.
  Lemma plus_negate_l : forall x, -x + x = 0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
forall x : R, - x + x = 0
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
forall x : R, - x + x = 0 exact left_inverse. Qed.

  Lemma negate_swap_r : forall x y, x - y = -(y - x).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
forall x y : R, x - y = - (y - x)
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
forall x y : R, x - y = - (y - x)
  intros.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
x - y = - (y - x)
  rewrite groups.negate_sg_op.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
x - y = sg_op (- - x) (- y)
  rewrite involutive.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
x - y = sg_op x (- y)
  reflexivity.
  Qed.

  Lemma negate_swap_l x y : -x + y = -(x - y).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
- x + y = - (x - y)
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
- x + y = - (x - y)
  rewrite groups.negate_sg_op_distr,involutive.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
- x + y = sg_op (- x) y
  reflexivity.
  Qed.

  Lemma negate_plus_distr : forall x y, -(x + y) = -x + -y.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
forall x y : R, - (x + y) = - x - y
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
forall x y : R, - (x + y) = - x - y exact groups.negate_sg_op_distr. Qed.

  Lemma negate_mult_l x : -x = - 1 * x.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
- x = -1 * x
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
- x = -1 * x
  apply (left_cancellation (+) x).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
x - x = x + -1 * x
  path_via 0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
x - x = 0
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
0 = x + -1 * x
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
x - x = 0 apply right_inverse.
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
0 = x + -1 * x path_via (1 * x + (- 1) * x).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
0 = 1 * x + -1 * x
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
1 * x + -1 * x = x + -1 * x
    +R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
0 = 1 * x + -1 * x apply symmetry.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
1 * x + -1 * x = 0
      rewrite <-distribute_r.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
(1 - 1) * x = 0 rewrite right_inverse.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
mon_unit * x = 0
      apply left_absorb.
    +R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
1 * x + -1 * x = x + -1 * x apply ap011;try reflexivity.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
1 * x = x
      apply left_identity.
  Qed.

  Lemma negate_mult_r x : -x = x * -1.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
- x = x * -1
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
- x = x * -1
    apply (right_cancellation (+) x).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
- x + x = x * -1 + x
    transitivity (x * -1 + x * 1).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
- x + x = x * -1 + x * 1
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
x * -1 + x * 1 = x * -1 + x
    -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
- x + x = x * -1 + x * 1 lhs apply left_inverse.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
mon_unit = x * -1 + x * 1
      rhs_V rapply simple_distribute_l.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
mon_unit = x * (-1 + 1)
      lhs_V rapply (right_absorb x).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
x * 0 = x * (-1 + 1)
      apply (ap (x *.)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
0 = -1 + 1
      symmetry.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
-1 + 1 = 0
      apply left_inverse.
    -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
x * -1 + x * 1 = x * -1 + x f_ap.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
x * 1 = x
      apply right_identity.
  Defined.

  Lemma negate_mult_distr_l x y : -(x * y) = -x * y.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
- (x * y) = - x * y
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
- (x * y) = - x * y
    lhs nrapply negate_mult_l.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
-1 * (x * y) = - x * y
    lhs rapply (simple_associativity (f := (.*.)) (-1) x y).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
-1 * x * y = - x * y
    apply (ap (.* y)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
-1 * x = - x
    symmetry.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
- x = -1 * x
    apply negate_mult_l.
  Defined.

  Lemma negate_mult_distr_r x y : -(x * y) = x * -y.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
- (x * y) = x * - y
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
- (x * y) = x * - y
    lhs nrapply negate_mult_r.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
x * y * -1 = x * - y
    lhs_V rapply (simple_associativity (f := (.*.)) x y).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
x * (y * -1) = x * - y
    apply (ap (x *.)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
y * -1 = - y
    symmetry.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
- y = y * -1
    apply negate_mult_r.
  Defined.

  Lemma negate_mult_negate x y : -x * -y = x * y.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
- x * - y = x * y
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
- x * - y = x * y
  rewrite <-negate_mult_distr_l, <-negate_mult_distr_r.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
- - (x * y) = x * y
  apply involutive.
  Qed.

  Lemma negate_0: -0 = 0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
- 0 = 0
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
- 0 = 0 exact groups.negate_mon_unit. Qed.

  Global Instance minus_0_r: RightIdentity (fun x y => x - y) 0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
RightIdentity (fun x y : R => x - y) 0
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
RightIdentity (fun x y : R => x - y) 0
  intro x; rewrite negate_0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
x + 0 = x apply right_identity.
  Qed.

  Lemma equal_by_zero_sum x y : x - y = 0 <-> x = y.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
x - y = 0 <-> x = y
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
x - y = 0 <-> x = y
  split; intros E.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: x - y = 0
x = y
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: x = y
x - y = 0
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: x - y = 0
x = y rewrite <- (left_identity y).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: x - y = 0
x = sg_op mon_unit y
    change (sg_op ?x ?y) with (0 + y).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: x - y = 0
x = 0 + y
    rewrite <- E.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: x - y = 0
x = x - y + y
    rewrite <-simple_associativity.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: x - y = 0
x = x + (- y + y)
    rewrite left_inverse.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: x - y = 0
x = x + mon_unit
    apply symmetry,right_identity.
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: x = y
x - y = 0 rewrite E.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: x = y
y - y = 0 apply right_inverse.
  Qed.

  Lemma flip_negate x y : -x = y <-> x = -y.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
- x = y <-> x = - y
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
- x = y <-> x = - y
  split; intros E.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: - x = y
x = - y
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: x = - y
- x = y
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: - x = y
x = - y rewrite <-E, involutive.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: - x = y
x = x trivial.
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: x = - y
- x = y rewrite E, involutive.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: x = - y
y = y trivial.
  Qed.

  Lemma flip_negate_0 x : -x = 0 <-> x = 0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
- x = 0 <-> x = 0
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
- x = 0 <-> x = 0
  etransitivity.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
- x = 0 <-> ?Goal
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
?Goal <-> x = 0
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
- x = 0 <-> ?Goal apply flip_negate.
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
x = - 0 <-> x = 0 rewrite negate_0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
x = 0 <-> x = 0
    apply reflexivity.
  Qed.

  Lemma flip_negate_ne_0 x : -x <> 0 <-> x <> 0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
- x <> 0 <-> x <> 0
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
- x <> 0 <-> x <> 0
  split; intros E ?; apply E; apply flip_negate_0;trivial.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
E: - x <> 0
X: x = 0
- - x = 0
  path_via x.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x: R
E: - x <> 0
X: x = 0
- - x = x apply involutive.
  Qed.

  Lemma negate_zero_prod_l x y : -x * y = 0 <-> x * y = 0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
- x * y = 0 <-> x * y = 0
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
- x * y = 0 <-> x * y = 0
  split; intros E.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: - x * y = 0
x * y = 0
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: x * y = 0
- x * y = 0
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: - x * y = 0
x * y = 0 apply (injective (-)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: - x * y = 0
- (x * y) = - 0 rewrite negate_mult_distr_l, negate_0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: - x * y = 0
- x * y = 0 trivial.
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: x * y = 0
- x * y = 0 apply (injective (-)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: x * y = 0
- (- x * y) = - 0
    rewrite negate_mult_distr_l, negate_involutive, negate_0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: x * y = 0
x * y = 0
    trivial.
  Qed.

  Lemma negate_zero_prod_r x y : x * -y = 0 <-> x * y = 0.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
x * - y = 0 <-> x * y = 0
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
x * - y = 0 <-> x * y = 0
    etransitivity.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
x * - y = 0 <-> ?Goal
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
?Goal <-> x * y = 0
    2: apply negate_zero_prod_l.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
x * - y = 0 <-> - x * y = 0
    split.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
x * - y = 0 -> - x * y = 0
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
- x * y = 0 -> x * - y = 0
    -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
x * - y = 0 -> - x * y = 0 intros E.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: x * - y = 0
- x * y = 0
      lhs_V nrapply negate_mult_distr_l.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: x * - y = 0
- (x * y) = 0 
      lhs nrapply negate_mult_distr_r.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: x * - y = 0
x * - y = 0
      exact E.
    -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
- x * y = 0 -> x * - y = 0 intros E.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: - x * y = 0
x * - y = 0
      lhs_V nrapply negate_mult_distr_r.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: - x * y = 0
- (x * y) = 0
      lhs nrapply negate_mult_distr_l.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
x, y: R
E: - x * y = 0
- x * y = 0
      exact E.
  Defined.

  Context `{!NoZeroDivisors R} `{forall x y:R, Stable (x = y)}.

  Global Instance mult_left_cancel:  forall z, PropHolds (z <> 0) ->
    LeftCancellation (.*.) z.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
forall z : R,
PropHolds (z <> 0) -> LeftCancellation mult z
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
forall z : R,
PropHolds (z <> 0) -> LeftCancellation mult z
  intros z z_nonzero x y E.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
z_nonzero: PropHolds (z <> 0)
x, y: R
E: z * x = z * y
x = y
  apply stable.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
z_nonzero: PropHolds (z <> 0)
x, y: R
E: z * x = z * y
~~ (x = y)
  intro U.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
z_nonzero: PropHolds (z <> 0)
x, y: R
E: z * x = z * y
U: x <> y
Empty
  apply (mult_ne_0 z (x - y) (is_ne_0 z)).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
z_nonzero: PropHolds (z <> 0)
x, y: R
E: z * x = z * y
U: x <> y
PropHolds (x - y <> 0)
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
z_nonzero: PropHolds (z <> 0)
x, y: R
E: z * x = z * y
U: x <> y
z * (x - y) = 0
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
z_nonzero: PropHolds (z <> 0)
x, y: R
E: z * x = z * y
U: x <> y
PropHolds (x - y <> 0) intro.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
z_nonzero: PropHolds (z <> 0)
x, y: R
E: z * x = z * y
U: x <> y
X: x - y = 0
Empty apply U.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
z_nonzero: PropHolds (z <> 0)
x, y: R
E: z * x = z * y
U: x <> y
X: x - y = 0
x = y apply equal_by_zero_sum.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
z_nonzero: PropHolds (z <> 0)
x, y: R
E: z * x = z * y
U: x <> y
X: x - y = 0
x - y = 0 trivial.
  -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
z_nonzero: PropHolds (z <> 0)
x, y: R
E: z * x = z * y
U: x <> y
z * (x - y) = 0 rewrite distribute_l, E.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
z_nonzero: PropHolds (z <> 0)
x, y: R
E: z * x = z * y
U: x <> y
z * y + z * - y = 0
    rewrite <-simple_distribute_l,right_inverse.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
z_nonzero: PropHolds (z <> 0)
x, y: R
E: z * x = z * y
U: x <> y
z * mon_unit = 0
    apply right_absorb.
  Qed.

  Instance mult_ne_0' `{!NoZeroDivisors R} x y
    : PropHolds (x <> 0) -> PropHolds (y <> 0) -> PropHolds (x * y <> 0).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
NoZeroDivisors1: NoZeroDivisors R
x, y: R
PropHolds (x <> 0) ->
PropHolds (y <> 0) -> PropHolds (x * y <> 0)
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
NoZeroDivisors1: NoZeroDivisors R
x, y: R
PropHolds (x <> 0) ->
PropHolds (y <> 0) -> PropHolds (x * y <> 0)
  intros Ex Ey Exy.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
NoZeroDivisors1: NoZeroDivisors R
x, y: R
Ex: PropHolds (x <> 0)
Ey: PropHolds (y <> 0)
Exy: x * y = 0
Empty
  unfold PropHolds in *.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
NoZeroDivisors1: NoZeroDivisors R
x, y: R
Ex: x <> 0
Ey: y <> 0
Exy: x * y = 0
Empty
  apply (no_zero_divisors x); split; eauto.
  Qed.

  Global Instance mult_right_cancel : forall z, PropHolds (z <> 0) ->
    RightCancellation (.*.) z.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
forall z : R,
PropHolds (z <> 0) -> RightCancellation mult z
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
forall z : R,
PropHolds (z <> 0) -> RightCancellation mult z
    intros z ? x y p.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
X: PropHolds (z <> 0)
x, y: R
p: x * z = y * z
x = y
    apply stable.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
X: PropHolds (z <> 0)
x, y: R
p: x * z = y * z
~~ (x = y)
    intro U.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
X: PropHolds (z <> 0)
x, y: R
p: x * z = y * z
U: x <> y
Empty
    nrapply (mult_ne_0' (x - y) z).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
X: PropHolds (z <> 0)
x, y: R
p: x * z = y * z
U: x <> y
NoZeroDivisors R
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
X: PropHolds (z <> 0)
x, y: R
p: x * z = y * z
U: x <> y
PropHolds (x - y <> 0)
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
X: PropHolds (z <> 0)
x, y: R
p: x * z = y * z
U: x <> y
PropHolds (z <> 0)
R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
X: PropHolds (z <> 0)
x, y: R
p: x * z = y * z
U: x <> y
(x - y) * z = 0
    -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
X: PropHolds (z <> 0)
x, y: R
p: x * z = y * z
U: x <> y
NoZeroDivisors R exact _.
    -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
X: PropHolds (z <> 0)
x, y: R
p: x * z = y * z
U: x <> y
PropHolds (x - y <> 0) intros r.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
X: PropHolds (z <> 0)
x, y: R
p: x * z = y * z
U: x <> y
r: x - y = 0
Empty
      apply U, equal_by_zero_sum, r.
    -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
X: PropHolds (z <> 0)
x, y: R
p: x * z = y * z
U: x <> y
PropHolds (z <> 0) exact _.
    -R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
X: PropHolds (z <> 0)
x, y: R
p: x * z = y * z
U: x <> y
(x - y) * z = 0 lhs rapply ring_dist_right.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
X: PropHolds (z <> 0)
x, y: R
p: x * z = y * z
U: x <> y
x * z + - y * z = 0
      rewrite <- negate_mult_distr_l.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
X: PropHolds (z <> 0)
x, y: R
p: x * z = y * z
U: x <> y
x * z - y * z = 0
      apply equal_by_zero_sum in p.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
z: R
X: PropHolds (z <> 0)
x, y: R
p: x * z - y * z = 0
U: x <> y
x * z - y * z = 0
      exact p.
  Defined.

  Lemma plus_conjugate x y : x = y + x - y.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
x, y: R
x = y + x - y
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
x, y: R
x = y + x - y
    rewrite (commutativity (f := (+)) y x),
      <- (simple_associativity (f := (+)) x y (-y)),
      right_inverse, right_identity.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
x, y: R
x = x
    reflexivity.
  Qed.

  Lemma plus_conjugate_alt x y : x = y + (x - y).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
x, y: R
x = y + (x - y)
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
x, y: R
x = y + (x - y)
    rewrite (simple_associativity (f := (+))).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsRing R
NoZeroDivisors0: NoZeroDivisors R
H0: forall x y : R, Stable (x = y)
x, y: R
x = y + x - y
    apply plus_conjugate.
  Qed.
End ring_props.

Section integral_domain_props.
  Context `{IsIntegralDomain R}.

  Instance intdom_nontrivial_apart `{Apart R} `{!TrivialApart R} :
    PropHolds (1 ≶ 0).R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsIntegralDomain R
H0: Apart R
TrivialApart0: TrivialApart R
PropHolds (1 ≶ 0)
  Proof.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsIntegralDomain R
H0: Apart R
TrivialApart0: TrivialApart R
PropHolds (1 ≶ 0)
  apply apartness.ne_apart.R: Type
Aplus: Plus R
Amult: Mult R
Azero: Zero R
Aone: One R
Anegate: Negate R
H: IsIntegralDomain R
H0: Apart R
TrivialApart0: TrivialApart R
PropHolds (1 <> 0) solve_propholds.
  Qed.
End integral_domain_props.

(* Due to bug #2528 *)
#[export]
Hint Extern 6 (PropHolds (1 ≶ 0)) =>
  eapply @intdom_nontrivial_apart : typeclass_instances.

Section ringmor_props.
  Context `{IsRing A} `{IsRing B} `{!IsSemiRingPreserving (f : A -> B)}.

  Definition preserves_negate x : f (-x) = -f x := groups.preserves_negate x.
  (* alias for convenience *)

  Lemma preserves_minus x y : f (x - y) = f x - f y.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsRing A
B: Type
Aplus0: Plus B
Amult0: Mult B
Azero0: Zero B
Aone0: One B
Anegate0: Negate B
H0: IsRing B
f: A -> B
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : A -> B)
x, y: A
f (x - y) = f x - f y
  Proof.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsRing A
B: Type
Aplus0: Plus B
Amult0: Mult B
Azero0: Zero B
Aone0: One B
Anegate0: Negate B
H0: IsRing B
f: A -> B
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : A -> B)
x, y: A
f (x - y) = f x - f y
  rewrite <-preserves_negate.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsRing A
B: Type
Aplus0: Plus B
Amult0: Mult B
Azero0: Zero B
Aone0: One B
Anegate0: Negate B
H0: IsRing B
f: A -> B
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : A -> B)
x, y: A
f (x - y) = f x + f (- y)
  apply preserves_plus.
  Qed.

  Lemma injective_preserves_0 : (forall x, f x = 0 -> x = 0) -> IsInjective f.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsRing A
B: Type
Aplus0: Plus B
Amult0: Mult B
Azero0: Zero B
Aone0: One B
Anegate0: Negate B
H0: IsRing B
f: A -> B
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : A -> B)
(forall x : A, f x = 0 -> x = 0) -> IsInjective f
  Proof.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsRing A
B: Type
Aplus0: Plus B
Amult0: Mult B
Azero0: Zero B
Aone0: One B
Anegate0: Negate B
H0: IsRing B
f: A -> B
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : A -> B)
(forall x : A, f x = 0 -> x = 0) -> IsInjective f
  intros E1 x y E.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsRing A
B: Type
Aplus0: Plus B
Amult0: Mult B
Azero0: Zero B
Aone0: One B
Anegate0: Negate B
H0: IsRing B
f: A -> B
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : A -> B)
E1: forall x : A, f x = 0 -> x = 0
x, y: A
E: f x = f y
x = y
  apply equal_by_zero_sum.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsRing A
B: Type
Aplus0: Plus B
Amult0: Mult B
Azero0: Zero B
Aone0: One B
Anegate0: Negate B
H0: IsRing B
f: A -> B
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : A -> B)
E1: forall x : A, f x = 0 -> x = 0
x, y: A
E: f x = f y
x - y = 0
  apply E1.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsRing A
B: Type
Aplus0: Plus B
Amult0: Mult B
Azero0: Zero B
Aone0: One B
Anegate0: Negate B
H0: IsRing B
f: A -> B
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : A -> B)
E1: forall x : A, f x = 0 -> x = 0
x, y: A
E: f x = f y
f (x - y) = 0
  rewrite preserves_minus, E.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsRing A
B: Type
Aplus0: Plus B
Amult0: Mult B
Azero0: Zero B
Aone0: One B
Anegate0: Negate B
H0: IsRing B
f: A -> B
IsSemiRingPreserving0: IsSemiRingPreserving
  (f : A -> B)
E1: forall x : A, f x = 0 -> x = 0
x, y: A
E: f x = f y
f y - f y = 0
  apply right_inverse.
  Qed.
End ringmor_props.

Section from_another_ring.
  Context `{IsCRing A} `{IsHSet B}
   `{Bplus : Plus B} `{Zero B} `{Bmult : Mult B} `{One B} `{Bnegate : Negate B}
    (f : B -> A) `{!IsInjective f}
    (plus_correct : forall x y, f (x + y) = f x + f y) (zero_correct : f 0 = 0)
    (mult_correct : forall x y, f (x * y) = f x * f y) (one_correct : f 1 = 1)
    (negate_correct : forall x, f (-x) = -f x).

  Lemma projected_ring: IsCRing B.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing A
B: Type
IsHSet0: IsHSet B
Bplus: Plus B
H0: Zero B
Bmult: Mult B
H1: One B
Bnegate: Negate B
f: B -> A
IsInjective0: IsInjective f
plus_correct: forall x y : B, f (x + y) = f x + f y
zero_correct: f 0 = 0
mult_correct: forall x y : B, f (x * y) = f x * f y
one_correct: f 1 = 1
negate_correct: forall x : B, f (- x) = - f x
IsCRing B
  Proof.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing A
B: Type
IsHSet0: IsHSet B
Bplus: Plus B
H0: Zero B
Bmult: Mult B
H1: One B
Bnegate: Negate B
f: B -> A
IsInjective0: IsInjective f
plus_correct: forall x y : B, f (x + y) = f x + f y
zero_correct: f 0 = 0
mult_correct: forall x y : B, f (x * y) = f x * f y
one_correct: f 1 = 1
negate_correct: forall x : B, f (- x) = - f x
IsCRing B
  split.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing A
B: Type
IsHSet0: IsHSet B
Bplus: Plus B
H0: Zero B
Bmult: Mult B
H1: One B
Bnegate: Negate B
f: B -> A
IsInjective0: IsInjective f
plus_correct: forall x y : B, f (x + y) = f x + f y
zero_correct: f 0 = 0
mult_correct: forall x y : B, f (x * y) = f x * f y
one_correct: f 1 = 1
negate_correct: forall x : B, f (- x) = - f x
IsAbGroup B
A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing A
B: Type
IsHSet0: IsHSet B
Bplus: Plus B
H0: Zero B
Bmult: Mult B
H1: One B
Bnegate: Negate B
f: B -> A
IsInjective0: IsInjective f
plus_correct: forall x y : B, f (x + y) = f x + f y
zero_correct: f 0 = 0
mult_correct: forall x y : B, f (x * y) = f x * f y
one_correct: f 1 = 1
negate_correct: forall x : B, f (- x) = - f x
IsCommutativeMonoid B
A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing A
B: Type
IsHSet0: IsHSet B
Bplus: Plus B
H0: Zero B
Bmult: Mult B
H1: One B
Bnegate: Negate B
f: B -> A
IsInjective0: IsInjective f
plus_correct: forall x y : B, f (x + y) = f x + f y
zero_correct: f 0 = 0
mult_correct: forall x y : B, f (x * y) = f x * f y
one_correct: f 1 = 1
negate_correct: forall x : B, f (- x) = - f x
LeftDistribute mult plus
  -A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing A
B: Type
IsHSet0: IsHSet B
Bplus: Plus B
H0: Zero B
Bmult: Mult B
H1: One B
Bnegate: Negate B
f: B -> A
IsInjective0: IsInjective f
plus_correct: forall x y : B, f (x + y) = f x + f y
zero_correct: f 0 = 0
mult_correct: forall x y : B, f (x * y) = f x * f y
one_correct: f 1 = 1
negate_correct: forall x : B, f (- x) = - f x
IsAbGroup B apply (groups.projected_ab_group f);assumption.
  -A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing A
B: Type
IsHSet0: IsHSet B
Bplus: Plus B
H0: Zero B
Bmult: Mult B
H1: One B
Bnegate: Negate B
f: B -> A
IsInjective0: IsInjective f
plus_correct: forall x y : B, f (x + y) = f x + f y
zero_correct: f 0 = 0
mult_correct: forall x y : B, f (x * y) = f x * f y
one_correct: f 1 = 1
negate_correct: forall x : B, f (- x) = - f x
IsCommutativeMonoid B apply (groups.projected_com_monoid f mult_correct one_correct);assumption.
  -A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing A
B: Type
IsHSet0: IsHSet B
Bplus: Plus B
H0: Zero B
Bmult: Mult B
H1: One B
Bnegate: Negate B
f: B -> A
IsInjective0: IsInjective f
plus_correct: forall x y : B, f (x + y) = f x + f y
zero_correct: f 0 = 0
mult_correct: forall x y : B, f (x * y) = f x * f y
one_correct: f 1 = 1
negate_correct: forall x : B, f (- x) = - f x
LeftDistribute mult plus repeat intro; apply (injective f).A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing A
B: Type
IsHSet0: IsHSet B
Bplus: Plus B
H0: Zero B
Bmult: Mult B
H1: One B
Bnegate: Negate B
f: B -> A
IsInjective0: IsInjective f
plus_correct: forall x y : B, f (x + y) = f x + f y
zero_correct: f 0 = 0
mult_correct: forall x y : B, f (x * y) = f x * f y
one_correct: f 1 = 1
negate_correct: forall x : B, f (- x) = - f x
a, b, c: B
f (a * (b + c)) = f (a * b + a * c)
    rewrite plus_correct, !mult_correct, plus_correct.A: Type
Aplus: Plus A
Amult: Mult A
Azero: Zero A
Aone: One A
Anegate: Negate A
H: IsCRing A
B: Type
IsHSet0: IsHSet B
Bplus: Plus B
H0: Zero B
Bmult: Mult B
H1: One B
Bnegate: Negate B
f: B -> A
IsInjective0: IsInjective f
plus_correct: forall x y : B, f (x + y) = f x + f y
zero_correct: f 0 = 0
mult_correct: forall x y : B, f (x * y) = f x * f y
one_correct: f 1 = 1
negate_correct: forall x : B, f (- x) = - f x
a, b, c: B
f a * (f b + f c) = f a * f b + f a * f c
    apply distribute_l.
  Qed.
End from_another_ring.

(* Section from_stdlib_semiring_theory.
  Context
    `(H: @semi_ring_theory R Rzero Rone Rplus Rmult Re)
    `{!@Setoid R Re}
    `{!Proper (Re ==> Re ==> Re) Rplus}
    `{!Proper (Re ==> Re ==> Re) Rmult}.

  Add Ring R2: H.

  Definition from_stdlib_semiring_theory: @SemiRing R Re Rplus Rmult Rzero Rone.
  Proof.
   repeat (constructor; try assumption); repeat intro
   ; unfold equiv, mon_unit, sg_op, zero_is_mon_unit, plus_is_sg_op,
     one_is_mon_unit, mult_is_sg_op, zero, mult, plus; ring.
  Qed.
End from_stdlib_semiring_theory.

Section from_stdlib_ring_theory.
  Context
    `(H: @ring_theory R Rzero Rone Rplus Rmult Rminus Rnegate Re)
    `{!@Setoid R Re}
    `{!Proper (Re ==> Re ==> Re) Rplus}
    `{!Proper (Re ==> Re ==> Re) Rmult}
    `{!Proper (Re ==> Re) Rnegate}.

  Add Ring R3: H.

  Definition from_stdlib_ring_theory: @Ring R Re Rplus Rmult Rzero Rone Rnegate.
  Proof.
   repeat (constructor; try assumption); repeat intro
   ; unfold equiv, mon_unit, sg_op, zero_is_mon_unit, plus_is_sg_op,
     one_is_mon_unit, mult_is_sg_op, mult, plus, negate; ring.
  Qed.
End from_stdlib_ring_theory. *)

Global Instance id_sr_morphism `{IsSemiCRing A}: IsSemiRingPreserving (@id A) := {}.

Section morphism_composition.
  Context `{Mult A} `{Plus A} `{One A} `{Zero A}
    `{Mult B} `{Plus B} `{One B} `{Zero B}
    `{Mult C} `{Plus C} `{One C} `{Zero C}
    (f : A -> B) (g : B -> C).

  Instance compose_sr_morphism:
    IsSemiRingPreserving f -> IsSemiRingPreserving g -> IsSemiRingPreserving (g ∘ f).A: Type
H: Mult A
H0: Plus A
H1: One A
H2: Zero A
B: Type
H3: Mult B
H4: Plus B
H5: One B
H6: Zero B
C: Type
H7: Mult C
H8: Plus C
H9: One C
H10: Zero C
f: A -> B
g: B -> C
IsSemiRingPreserving f ->
IsSemiRingPreserving g -> IsSemiRingPreserving (g ∘ f)
  Proof.A: Type
H: Mult A
H0: Plus A
H1: One A
H2: Zero A
B: Type
H3: Mult B
H4: Plus B
H5: One B
H6: Zero B
C: Type
H7: Mult C
H8: Plus C
H9: One C
H10: Zero C
f: A -> B
g: B -> C
IsSemiRingPreserving f ->
IsSemiRingPreserving g -> IsSemiRingPreserving (g ∘ f)
  split; apply _.
  Qed.

  Instance invert_sr_morphism:
    forall `{!IsEquiv f}, IsSemiRingPreserving f -> IsSemiRingPreserving (f^-1).A: Type
H: Mult A
H0: Plus A
H1: One A
H2: Zero A
B: Type
H3: Mult B
H4: Plus B
H5: One B
H6: Zero B
C: Type
H7: Mult C
H8: Plus C
H9: One C
H10: Zero C
f: A -> B
g: B -> C
forall IsEquiv0 : IsEquiv f,
IsSemiRingPreserving f -> IsSemiRingPreserving f^-1
  Proof.A: Type
H: Mult A
H0: Plus A
H1: One A
H2: Zero A
B: Type
H3: Mult B
H4: Plus B
H5: One B
H6: Zero B
C: Type
H7: Mult C
H8: Plus C
H9: One C
H10: Zero C
f: A -> B
g: B -> C
forall IsEquiv0 : IsEquiv f,
IsSemiRingPreserving f -> IsSemiRingPreserving f^-1
  split; apply _.
  Qed.
End morphism_composition.

#[export]
Hint Extern 4 (IsSemiRingPreserving (_ ∘ _)) =>
  class_apply @compose_sr_morphism : typeclass_instances.
#[export]
Hint Extern 4 (IsSemiRingPreserving (_^-1)) =>
  class_apply @invert_sr_morphism : typeclass_instances.