-axiom q_le_minus: ∀a,b,c:ℚ. a ≤ c - b → a + b ≤ c.
-axiom q_le_minus_r: ∀a,b,c:ℚ. a - b ≤ c → a ≤ c + b.
-axiom q_lt_plus: ∀a,b,c:ℚ. a - b < c → a < c + b.
-axiom q_lt_minus: ∀a,b,c:ℚ. a + b < c → a < c - b.
+inductive q_le_elimination (a,b:ℚ) : CProp ≝
+| q_le_from_eq : a = b → q_le_elimination a b
+| q_le_from_lt : a < b → q_le_elimination a b.
+
+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.
+axiom q_lt_plus_r: ∀a,b,c:ℚ. a - b < c → a < c + b.
+