fact: Record SOR : Type := mk_SOR_theory { SORsetoid : Setoid_Theory R req; SORplus_wd : forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 + y1 == x2 + y2; SORtimes_wd : forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> x1 * y1 == x2 * y2; SORopp_wd : forall x1 x2, x1 == x2 -> -x1 == -x2; SORle_wd : forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> (x1 <= y1 <-> x2 <= y2); SORlt_wd : forall x1 x2, x1 == x2 -> forall y1 y2, y1 == y2 -> (x1 < y1 <-> x2 < y2); SORrt : ring_theory rO rI rplus rtimes rminus ropp req; SORle_refl : forall n : R, n <= n; SORle_antisymm : forall n m : R, n <= m -> m <= n -> n == m; SORle_trans : forall n m p : R, n <= m -> m <= p -> n <= p; SORlt_le_neq : forall n m : R, n < m <-> n <= m /\ n ~= m; SORlt_trichotomy : forall n m : R, n < m \/ n == m \/ m < n; SORplus_le_mono_l : forall n m p : R, n <= m -> p + n <= p + m; SORtimes_pos_pos : forall n m : R, 0 < n -> 0 < m -> 0 < n * m; SORneq_0_1 : 0 ~= 1 }.
imports: Setoid Ring