some more work to factorize out uninteresting parts of the proof...

[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 2073c8a77afad47f5b6d6c64b56464a1db1ff0a0..9d73f7ab9b209fdfa887c3aed98764d3cd737265 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/q_support.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_support.ma
@@ -109,3 +109,17 @@ 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.