X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fmodels%2Fq_support.ma;h=4f27f398a42d9963a35f31c08e903666ec403d73;hb=b12a46d53cf80d40b253ca5dd495397c5c0b4287;hp=70b3e6ade4b21544c6385be1d58b313167f50ec8;hpb=80ea6f314e89d9d280338c41860cb04949319629;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 70b3e6ade..4f27f398a 100644
--- a/helm/software/matita/contribs/dama/dama/models/q_support.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_support.ma
@@ -48,6 +48,8 @@ inductive q_le_elimination (a,b:ℚ) : CProp ≝
 
 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.