Require Import
  HoTT.Classes.interfaces.abstract_algebra
  HoTT.Classes.interfaces.orders
  HoTT.Classes.theory.dec_fields.
[Loading ML file number_string_notation_plugin.cmxs (using legacy method) ... done]
Require Export
  HoTT.Classes.orders.rings.

Generalizable Variables F f R Fle Flt.

Section contents.
Context `{IsDecField F} `{Apart F} `{!TrivialApart F}
  `{!FullPseudoSemiRingOrder Fle Flt} `{DecidablePaths F}.
(* Add Ring F : (stdlib_ring_theory F). *)

Instance pos_dec_recip_compat x : PropHolds (0 < x) -> PropHolds (0 < /x).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
PropHolds (0 < x) -> PropHolds (0 < / x)
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
PropHolds (0 < x) -> PropHolds (0 < / x)
intros E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
E: PropHolds (0 < x)
PropHolds (0 < / x)
apply (strictly_order_reflecting (x *.)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
E: PropHolds (0 < x)
x * 0 < x / x
rewrite dec_recip_inverse by (apply orders.lt_ne_flip;trivial).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
E: PropHolds (0 < x)
x * 0 < 1
rewrite mult_0_r.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
E: PropHolds (0 < x)
0 < 1 solve_propholds.
Qed.

Instance nonneg_dec_recip_compat x : PropHolds (0 ≤ x) -> PropHolds (0 ≤ /x).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
PropHolds (0 ≤ x) -> PropHolds (0 ≤ / x)
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
PropHolds (0 ≤ x) -> PropHolds (0 ≤ / x)
intros E.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
E: PropHolds (0 ≤ x)
PropHolds (0 ≤ / x) red.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
E: PropHolds (0 ≤ x)
0 ≤ / x
destruct (dec (x = 0)) as [E2 | E2].
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
E: PropHolds (0 ≤ x)
E2: x = 0
0 ≤ / x
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
E: PropHolds (0 ≤ x)
E2: x <> 0
0 ≤ / x
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
E: PropHolds (0 ≤ x)
E2: x = 0
0 ≤ / x rewrite E2, dec_recip_0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
E: PropHolds (0 ≤ x)
E2: x = 0
0 ≤ 0 rewrite E2 in E;trivial.
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
E: PropHolds (0 ≤ x)
E2: x <> 0
0 ≤ / x apply lt_le.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
E: PropHolds (0 ≤ x)
E2: x <> 0
PropHolds (0 < / x) apply pos_dec_recip_compat.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
E: PropHolds (0 ≤ x)
E2: x <> 0
PropHolds (0 < x)
  apply lt_iff_le_ne.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
E: PropHolds (0 ≤ x)
E2: x <> 0
((0 ≤ x) * (0 <> x))%type split;trivial.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
E: PropHolds (0 ≤ x)
E2: x <> 0
0 <> x
  apply symmetric_neq;trivial.
Qed.

Lemma neg_dec_recip_compat x : x < 0 -> /x < 0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
x < 0 -> / x < 0
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
x < 0 -> / x < 0
intros.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
X: x < 0
/ x < 0 apply flip_neg_negate.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
X: x < 0
0 < - / x
rewrite dec_recip_negate.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
X: x < 0
0 < / - x
apply pos_dec_recip_compat.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
X: x < 0
PropHolds (0 < - x)
apply flip_neg_negate.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
X: x < 0
x < 0 trivial.
Qed.

Lemma nonpos_dec_recip_compat x : x ≤ 0 -> /x ≤ 0.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
x ≤ 0 -> / x ≤ 0
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
x ≤ 0 -> / x ≤ 0
intros.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
X: x ≤ 0
/ x ≤ 0 apply flip_nonpos_negate.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
X: x ≤ 0
0 ≤ - / x
rewrite dec_recip_negate.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
X: x ≤ 0
0 ≤ / - x
apply nonneg_dec_recip_compat.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x: F
X: x ≤ 0
PropHolds (0 ≤ - x)
apply flip_nonpos_negate;trivial.
Qed.

Lemma flip_le_dec_recip x y : 0 < y -> y ≤ x  -> /x ≤ /y.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
0 < y -> y ≤ x -> / x ≤ / y
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
0 < y -> y ≤ x -> / x ≤ / y
intros E1 E2.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y ≤ x
/ x ≤ / y
apply (order_reflecting_pos (.*.) x).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y ≤ x
0 < x
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y ≤ x
x / x ≤ x / y
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y ≤ x
0 < x apply lt_le_trans with y;trivial.
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y ≤ x
x / x ≤ x / y rewrite dec_recip_inverse.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y ≤ x
1 ≤ x / y
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y ≤ x
x <> 0
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y ≤ x
1 ≤ x / y apply (order_reflecting_pos (.*.) y);trivial.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y ≤ x
y * 1 ≤ y * (x / y)
    rewrite (commutativity x), simple_associativity, dec_recip_inverse.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y ≤ x
y * 1 ≤ 1 * x
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y ≤ x
y <> 0
    *
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y ≤ x
y * 1 ≤ 1 * x rewrite mult_1_l,mult_1_r.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y ≤ x
y ≤ x trivial.
    *
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y ≤ x
y <> 0 apply lt_ne_flip;trivial.
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y ≤ x
x <> 0 apply lt_ne_flip.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y ≤ x
0 < x
    apply lt_le_trans with y;trivial.
Qed.

Lemma flip_le_dec_recip_l x y : 0 < y -> /y ≤ x  -> /x ≤ y.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
0 < y -> / y ≤ x -> / x ≤ y
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
0 < y -> / y ≤ x -> / x ≤ y
intros E1 E2.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: / y ≤ x
/ x ≤ y
rewrite <-(dec_recip_involutive y).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: / y ≤ x
/ x ≤ / / y
apply flip_le_dec_recip;trivial.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: / y ≤ x
0 < / y
apply pos_dec_recip_compat;trivial.
Qed.

Lemma flip_le_dec_recip_r x y : 0 < y -> y ≤ /x  -> x ≤ /y.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
0 < y -> y ≤ / x -> x ≤ / y
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
0 < y -> y ≤ / x -> x ≤ / y
intros E1 E2.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y ≤ / x
x ≤ / y
rewrite <-(dec_recip_involutive x).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y ≤ / x
/ / x ≤ / y
apply flip_le_dec_recip;trivial.
Qed.

Lemma flip_lt_dec_recip x y : 0 < y -> y < x  -> /x < /y.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
0 < y -> y < x -> / x < / y
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
0 < y -> y < x -> / x < / y
intros E1 E2.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y < x
/ x < / y
assert (0 < x) by (transitivity y;trivial).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y < x
X: 0 < x
/ x < / y
apply (strictly_order_reflecting (x *.)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y < x
X: 0 < x
x / x < x / y
rewrite dec_recip_inverse.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y < x
X: 0 < x
1 < x / y
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y < x
X: 0 < x
x <> 0
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y < x
X: 0 < x
1 < x / y apply (strictly_order_reflecting (y *.)).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y < x
X: 0 < x
y * 1 < y * (x / y)
  rewrite (commutativity x), simple_associativity, dec_recip_inverse.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y < x
X: 0 < x
y * 1 < 1 * x
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y < x
X: 0 < x
y <> 0
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y < x
X: 0 < x
y * 1 < 1 * x rewrite mult_1_l,mult_1_r.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y < x
X: 0 < x
y < x trivial.
  +
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y < x
X: 0 < x
y <> 0 apply lt_ne_flip.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y < x
X: 0 < x
0 < y trivial.
-
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y < x
X: 0 < x
x <> 0 apply lt_ne_flip;trivial.
Qed.

Lemma flip_lt_dec_recip_l x y : 0 < y -> /y < x  -> /x < y.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
0 < y -> / y < x -> / x < y
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
0 < y -> / y < x -> / x < y
intros E1 E2.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: / y < x
/ x < y
rewrite <-(dec_recip_involutive y).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: / y < x
/ x < / / y
apply flip_lt_dec_recip; trivial.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: / y < x
0 < / y
apply pos_dec_recip_compat.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: / y < x
PropHolds (0 < y) trivial.
Qed.

Lemma flip_lt_dec_recip_r x y : 0 < y -> y < /x  -> x < /y.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
0 < y -> y < / x -> x < / y
Proof.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
0 < y -> y < / x -> x < / y
intros E1 E2.
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y < / x
x < / y
rewrite <-(dec_recip_involutive x).
F: Type
Aplus: Plus F
Amult: Mult F
Azero: Zero F
Aone: One F
Anegate: Negate F
Adec_recip: DecRecip F
H: IsDecField F
H0: Apart F
TrivialApart0: TrivialApart F
Fle: Le F
Flt: Lt F
FullPseudoSemiRingOrder0: FullPseudoSemiRingOrder Fle
  Flt
H1: DecidablePaths F
x, y: F
E1: 0 < y
E2: y < / x
/ / x < / y
apply flip_lt_dec_recip;trivial.
Qed.
End contents.

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