shift almost done

[helm.git] / helm / software / matita / contribs / dama / dama / models / q_support.ma

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 f10113d501b9c640fa705f1e5db6d275f0a44cc4..b948e61b5d8dc1e936e499e82de27bbb1a26b44e 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/q_support.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_support.ma
@@ -33,6 +33,7 @@ axiom q_minus_r: ∀x,y. y + Qpos x = y - Qneg x.
 axiom q_plus_assoc: ∀x,y,z.x + (y + z) = x + y + z. 
 axiom q_elim_minus: ∀x,y.x - y = x + Qopp y.
 axiom q_elim_opp: ∀x,y.x - Qopp y = x + y.
+axiom q_minus_distrib:∀x,y,z:Q.x - (y + z) = x - y - z.
 
 (* order over Q *)
 axiom qlt : ℚ → ℚ → CProp.
@@ -51,7 +52,11 @@ 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.
 axiom q_lt_corefl: ∀x:Q.x < x → False.
@@ -59,6 +64,8 @@ axiom q_lt_antisym: ∀x,y:Q.x < y → y < x → False.
 axiom q_lt_le_incompat: ∀x,y:Q.x < y → y ≤ x → False.
 axiom q_neg_gt: ∀r:ratio.OQ < Qneg r → False.
 axiom q_lt_trans: ∀x,y,z:Q. x < y → y < z → x < z.
+axiom q_lt_le_trans: ∀x,y,z:Q. x < y → y ≤ z → x < z.
+axiom q_le_lt_trans: ∀x,y,z:Q. x ≤ y → y < z → x < z.
 axiom q_le_trans: ∀x,y,z:Q. x ≤ y → y ≤ z → x ≤ z.
 axiom q_pos_OQ: ∀x.Qpos x ≤ OQ → False.
 axiom q_lt_plus_trans: ∀x,y:Q.OQ ≤ x → OQ < y → OQ < x + y.
@@ -66,6 +73,8 @@ axiom q_pos_lt_OQ: ∀x.OQ < Qpos x.
 axiom q_le_plus_trans: ∀x,y:Q. OQ ≤ x → OQ ≤ y → OQ ≤ x + y.
 axiom q_le_S: ∀x,y,z.OQ ≤ x → x + y ≤ z → y ≤ z.
 axiom q_eq_to_le: ∀x,y. x = y → x ≤ y.
+axiom q_le_OQ_Qpos: ∀x.OQ ≤ Qpos x.
+       
 
 inductive q_le_elimination (a,b:ℚ) : CProp ≝
 | q_le_from_eq : a = b → q_le_elimination a b
@@ -88,3 +97,33 @@ axiom q_d_sym:  ∀x,y. ⅆ[x,y] = ⅆ[y,x].
 (* integral part *)
 axiom nat_of_q: ℚ → nat.
 
+(* derived *)
+lemma q_lt_canc_plus_r:
+  ∀x,y,z:Q.x + z < y + z → x < y.
+intros; rewrite < (q_plus_OQ y); rewrite < (q_plus_minus z);
+rewrite > q_elim_minus; rewrite > q_plus_assoc;
+apply q_lt_plus; rewrite > q_elim_opp; assumption;
+qed.
+
+lemma q_lt_inj_plus_r:
+  ∀x,y,z:Q.x < y → x + z < y + z.
+intros; apply (q_lt_canc_plus_r ?? (Qopp z));
+do 2 (rewrite < q_plus_assoc;rewrite < q_elim_minus);
+rewrite > q_plus_minus;
+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.