orders.dec_fields

Require Import
  Relation_Definitions Ring
  abstract_algebra interfaces.orders theory.rings theory.dec_fields.
Require Export
  orders.rings.

Section contents.
Context `{DecField F} `{Apart F} `{!TrivialApart F} `{!FullPseudoSemiRingOrder Fle Flt} `{ x y : F, Decision (x = y)}.
Add Ring F : (stdlib_ring_theory F).

Instance pos_dec_mult_inv_compat x : PropHolds (0 < x) PropHolds (0 < /x).

Instance nonneg_dec_mult_inv_compat x : PropHolds (0 x) PropHolds (0 /x).

Lemma neg_dec_mult_inv_compat x : x < 0 /x < 0.

Lemma nonpos_dec_mult_inv_compat x : x 0 /x 0.

Lemma flip_le_dec_mult_inv x y : 0 < y y x /x /y.

Lemma flip_le_dec_mult_inv_l x y : 0 < y /y x /x y.

Lemma flip_le_dec_mult_inv_r x y : 0 < y y /x x /y.

Lemma flip_lt_dec_mult_inv x y : 0 < y y < x /x < /y.

Lemma flip_lt_dec_mult_inv_l x y : 0 < y /y < x /x < y.

Lemma flip_lt_dec_mult_inv_r x y : 0 < y y < /x x < /y.
End contents.

Hint Extern 12 (PropHolds (0 _)) => eapply @nonneg_dec_mult_inv_compat : typeclass_instances.
Hint Extern 12 (PropHolds (0 < _)) => eapply @pos_dec_mult_inv_compat : typeclass_instances.