update in basic_2

[helm.git] / matita / matita / contribs / lambdadelta / basic_2 / static / sd.ma

diff --git a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma
index 63143b19b00e7f2012fe6fcdd492ac9e4c069de4..79d9f0740720505ebce4a59056ebee30a8b060f0 100644 (file)
--- a/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/static/sd.ma
@@ -82,7 +82,7 @@ definition sd_SO: ∀h. nat → sd h ≝ λh,k. mk_sd h (deg_SO h k) ….
 qed.
 
 let rec sd_l (h:sh) (k:nat) (l:nat) on l : sd h ≝
-   match l with 
+   match l with
    [ O   ⇒ sd_O h
    | S l ⇒ match l with
            [ O ⇒ sd_SO h k
@@ -100,6 +100,13 @@ lapply (deg_mono … H1 H2) -H1 -H2 #H
 <(associative_plus l 1 1) >H <plus_minus_m_m // /2 width=3 by transitive_le/
 qed.
 
+lemma deg_prec: ∀h,g,k,l,l0. deg h g ((next h)^l k) (l0+1) → deg h g k (l+l0+1).
+#h #g #k #l @(nat_ind_plus … l) -l //
+#l #IHl #l0 >iter_SO #H
+lapply (deg_pred … H) -H <(associative_plus l0 1 1) #H
+lapply (IHl … H) -IHl -H //
+qed.
+
 lemma sd_l_SS: ∀h,k,l. sd_l h k (l + 2) = sd_l h (next h k) (l + 1).
 #h #k #l <plus_n_Sm <plus_n_Sm //
 qed.