more work

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

diff --git a/helm/software/matita/contribs/dama/dama/models/q_function.ma b/helm/software/matita/contribs/dama/dama/models/q_function.ma
index bb3ba55fc8c49ff33bacbef1b8f5c2c6b8fd81f1..32122371004982cad24e4deccf33ec5f71dad0e1 100644 (file)
--- a/helm/software/matita/contribs/dama/dama/models/q_function.ma
+++ b/helm/software/matita/contribs/dama/dama/models/q_function.ma
@@ -64,16 +64,27 @@ whd in ⊢ (% → ?); simplify in H3;
         |2: cases n in H5 H6; [intros; reflexivity] intros;
             cases (?:False); clear H6; cases (bars l1) in H5; simplify; intros;
             [apply (q_pos_OQ one);|apply (q_pos_OQ (\fst b));] 
-            apply (q_le_S ??? (sum_bases_ge_OQ (mk_q_f init ?) n1));[apply [];|3:apply l]
-            simplify in ⊢ (? (? (? % ?) ?) ?); rewrite < (q_plus_minus w);
-            apply q_le_minus_r; rewrite < q_minus_r; 
-            rewrite < E in ⊢ (??%); assumption;]
+            apply (q_le_S ??? (sum_bases_ge_OQ ? n1));[apply []|3:apply l]
+            simplify in ⊢ (? (? (? % ?) ?) ?); rewrite < (q_plus_minus (Qpos w));
+            rewrite > q_elim_minus; apply q_le_minus_r; 
+            rewrite > q_elim_opp; rewrite < E in ⊢ (??%); assumption;]
     |2: intros; rewrite > H8; rewrite > H7; clear H8 H7;
         simplify in H5 H6 ⊢ %; 
         cases (\fst w1) in H5 H6; [intros; reflexivity]
         cases (bars l1);
         [1: intros; simplify; elim n [reflexivity] simplify; assumption;
-        |2: simplify; intros; cases (?:False);
+        |2: simplify; intros; cases (?:False); clear H6;
+            apply (q_lt_le_incompat (input - init) (Qpos w) );
+            [1: rewrite > H2; do 2 rewrite > q_elim_minus;
+                apply q_lt_plus; rewrite > q_elim_minus;
+                rewrite < q_plus_assoc; rewrite < q_elim_minus;
+                rewrite > q_plus_minus;
+                rewrite > q_plus_OQ; assumption;
+            |2: rewrite < q_d_noabs; [2: apply q_lt_to_le; assumption]
+                rewrite > q_d_sym; apply (q_le_S ???? H5);
+                apply sum_bases_ge_OQ;]]
+    |3:
+    
         
 STOP