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.
+axiom q_le_plus: ∀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_r: ∀a,b,c:ℚ. a + b < c → a < c - b.
+axiom q_lt_minus_r: ∀a,b,c:ℚ. a - b < c → a < c + b.
axiom q_lt_opp_opp: ∀a,b.b < a → Qopp a < Qopp b.
axiom q_lt_to_le: ∀a,b:ℚ.a < b → a ≤ b.
axiom q_le_to_diff_ge_OQ : ∀a,b.a ≤ b → OQ ≤ b-a.
do 2 rewrite > q_plus_OQ; assumption;
qed.
+lemma q_le_inj_plus_r:
+ ∀x,y,z:Q.x ≤ y → x + z ≤ y + z.
+intros;cases (q_le_cases ?? H);
+[1: rewrite > H1; apply q_eq_to_le; reflexivity;
+|2: apply q_lt_to_le; apply q_lt_inj_plus_r; assumption;]
+qed.
+
+lemma q_le_canc_plus_r:
+ ∀x,y,z:Q.x + z ≤ y + z → x ≤ y.
+intros; lapply (q_le_inj_plus_r ?? (Qopp z) H) as H1;
+do 2 rewrite < q_plus_assoc in H1;
+rewrite < q_elim_minus in H1; rewrite > q_plus_minus in H1;
+do 2 rewrite > q_plus_OQ in H1; assumption;
+qed.