X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fmodels%2Fq_support.ma;h=b948e61b5d8dc1e936e499e82de27bbb1a26b44e;hb=23dbce6cd7d599c10eb7801e91bc8b5164164418;hp=9d73f7ab9b209fdfa887c3aed98764d3cd737265;hpb=d309714a7f00acfae311fa24612e57e9be085ff3;p=helm.git

diff --git a/helm/software/matita/contribs/dama/dama/models/q_support.ma b/helm/software/matita/contribs/dama/dama/models/q_support.ma
index 9d73f7ab9..b948e61b5 100644
--- a/helm/software/matita/contribs/dama/dama/models/q_support.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_support.ma
@@ -52,6 +52,10 @@ 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.
+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.