include "Q/q/qtimes.ma".
include "Q/q/qplus.ma".
-include "cprop_connectives.ma".
+include "logic/cprop_connectives.ma".
-notation "\rationals" non associative with precedence 99 for @{'q}.
-interpretation "Q" 'q = Q.
+interpretation "Q" 'Q = Q.
(* group over Q *)
axiom qp : ℚ → ℚ → ℚ.
axiom q_le_cases : ∀x,y:ℚ.x ≤ y → q_le_elimination x y.
+axiom q_le_to_le_to_eq : ∀x,y. x ≤ y → y ≤ x → x = y.
+
axiom q_le_plus_l: ∀a,b,c:ℚ. a ≤ c - b → a + b ≤ c.
axiom q_le_plus_r: ∀a,b,c:ℚ. a - b ≤ c → a ≤ c + b.
axiom q_lt_plus_l: ∀a,b,c:ℚ. a < c - b → a + b < c.