From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 28 Jul 2018 13:40:56 +0000 (+0200)
Subject: update in ground_2 and basic_2
X-Git-Tag: make_still_working~292
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=1083ac3b1acac5f1ac1fa40a9a417dd9d268dced;p=helm.git

update in ground_2 and basic_2

+ modification in cnv allows to improve cnv_cpm_trans_lpr_aux
+ modification in lsubv allows to prove its transitivity
+ one lemma added to the arithmetic library
---

diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma
index bfa880d6c..398ef6783 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv.ma
@@ -24,7 +24,7 @@ inductive cnv (a) (h): relation3 genv lenv term ≝
 | cnv_zero: ∀I,G,K,V. cnv a h G K V → cnv a h G (K.ⓑ{I}V) (#0)
 | cnv_lref: ∀I,G,K,i. cnv a h G K (#i) → cnv a h G (K.ⓘ{I}) (#↑i)
 | cnv_bind: ∀p,I,G,L,V,T. cnv a h G L V → cnv a h G (L.ⓑ{I}V) T → cnv a h G L (ⓑ{p,I}V.T)
-| cnv_appl: ∀n,p,G,L,V,W0,T,U0. (a = Ⓣ → n = 1) → cnv a h G L V → cnv a h G L T →
+| cnv_appl: ∀n,p,G,L,V,W0,T,U0. (a = Ⓣ → n ≤ 1) → cnv a h G L V → cnv a h G L T →
             ⦃G, L⦄ ⊢ V ➡*[1, h] W0 → ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0 → cnv a h G L (ⓐV.T)
 | cnv_cast: ∀G,L,U,T,U0. cnv a h G L U → cnv a h G L T →
             ⦃G, L⦄ ⊢ U ➡*[h] U0 → ⦃G, L⦄ ⊢ T ➡*[1, h] U0 → cnv a h G L (ⓝU.T)
@@ -103,7 +103,7 @@ lemma cnv_inv_bind (a) (h): ∀p,I,G,L,V,T. ⦃G, L⦄ ⊢ ⓑ{p,I}V.T ![a, h] 
 /2 width=4 by cnv_inv_bind_aux/ qed-.
 
 fact cnv_inv_appl_aux (a) (h): ∀G,L,X. ⦃G, L⦄ ⊢ X ![a, h] → ∀V,T. X = ⓐV.T →
-                               ∃∃n,p,W0,U0. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
+                               ∃∃n,p,W0,U0. a = Ⓣ → n ≤ 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
                                             ⦃G, L⦄ ⊢ V ➡*[1, h] W0 & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0.
 #a #h #G #L #X * -L -X
 [ #G #L #s #X1 #X2 #H destruct
@@ -117,7 +117,7 @@ qed-.
 
 (* Basic_2A1: uses: snv_inv_appl *)
 lemma cnv_inv_appl (a) (h): ∀G,L,V,T. ⦃G, L⦄ ⊢ ⓐV.T ![a, h] →
-                            ∃∃n,p,W0,U0. a = Ⓣ → n = 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
+                            ∃∃n,p,W0,U0. a = Ⓣ → n ≤ 1 & ⦃G, L⦄ ⊢ V ![a, h] & ⦃G, L⦄ ⊢ T ![a, h] &
                                          ⦃G, L⦄ ⊢ V ➡*[1, h] W0 & ⦃G, L⦄ ⊢ T ➡*[n, h] ⓛ{p}W0.U0.
 /2 width=3 by cnv_inv_appl_aux/ qed-.
 
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma
index 2d9f53b9c..29d40c3ef 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/cnv_cpm_trans.ma
@@ -23,12 +23,12 @@ include "basic_2/dynamic/lsubv_cnv.ma".
 
 (* Properties with context-free parallel reduction for local environments *****)
 
-fact cnv_cpm_trans_lpr_aux (a) (h) (o): a = Ⓕ →
+fact cnv_cpm_trans_lpr_aux (a) (h) (o):
                            ∀G0,L0,T0.
                            (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpms_conf_lpr a h G1 L1 T1) →
                            (∀G1,L1,T1. ⦃G0, L0, T0⦄ >[h, o] ⦃G1, L1, T1⦄ → IH_cnv_cpm_trans_lpr a h G1 L1 T1) →
                            ∀G1,L1,T1. G0 = G1 → L0 = L1 → T0 = T1 → IH_cnv_cpm_trans_lpr a h G1 L1 T1.
-#a #h #o #Ha #G0 #L0 #T0 #IH2 #IH1 #G1 #L1 * * [|||| * ]
+#a #h #o #G0 #L0 #T0 #IH2 #IH1 #G1 #L1 * * [|||| * ]
 [ #s #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #_ destruct -IH2 -IH1 -H1
   elim (cpm_inv_sort1 … H2) -H2 * #H1 #H2 destruct //
 | #i #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct -IH2
@@ -69,7 +69,7 @@ fact cnv_cpm_trans_lpr_aux (a) (h) (o): a = Ⓕ →
     lapply (cpms_trans … HXV2 … HXW1) -XW1 <plus_n_O #HV2W1
     lapply (cpms_trans … HTU2 … (ⓛ{p}W1.U2) ?)
     [3:|*: /2 width=2 by cpms_bind/ ] -W2 <plus_n_O #HTU2
-    @(cnv_appl … HV2W1 HTU2) // #H destruct
+    /4 width=7 by cnv_appl, minus_le_trans_sn/
   | #q #V2 #W10 #W20 #T10 #T20 #HV12 #HW120 #HT120 #H1 #H2 destruct
     elim (cnv_inv_bind … HT1) -HT1 #HW10 #HT10
     elim (cpms_inv_abst_sn … HTU1) -HTU1 #W30 #T30 #HW130 #_ #H destruct -T30
@@ -102,7 +102,7 @@ fact cnv_cpm_trans_lpr_aux (a) (h) (o): a = Ⓕ →
     elim (cprs_conf … HXW32 … HW3) -W3 #W3 #HXW23 #HW3
     lapply (cpms_trans … HXVW2 … HXW23) -XW2 <plus_n_O #H1
     lapply (cpms_trans … HTU2 ? (ⓛ{p}W3.U2) ?) [3:|*:/2 width=2 by cpms_bind/ ] -W #H2
-    @cnv_bind // @(cnv_appl … H1 H2) // #H destruct
+    /5 width=7 by cnv_appl, cnv_bind, minus_le_trans_sn/
   ]
 | #W1 #T1 #HG0 #HL0 #HT0 #H1 #x #X #H2 #L2 #HL12 destruct
   elim (cnv_inv_cast … H1) -H1 #U1 #HW1 #HT1 #HWU1 #HTU1
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma
index bba857ac8..6549c361e 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv.ma
@@ -17,11 +17,10 @@ include "basic_2/dynamic/cnv.ma".
 
 (* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
 
-(* Note: this is not transitive *)
 inductive lsubv (a) (h) (G): relation lenv ≝
 | lsubv_atom: lsubv a h G (⋆) (⋆)
 | lsubv_bind: ∀I,L1,L2. lsubv a h G L1 L2 → lsubv a h G (L1.ⓘ{I}) (L2.ⓘ{I})
-| lsubv_beta: ∀L1,L2,W,V. ⦃G, L1⦄ ⊢ ⓝW.V ![a,h] → ⦃G, L2⦄ ⊢ W ![a,h] →
+| lsubv_beta: ∀L1,L2,W,V. ⦃G, L1⦄ ⊢ ⓝW.V ![a,h] →
               lsubv a h G L1 L2 → lsubv a h G (L1.ⓓⓝW.V) (L2.ⓛW)
 .
 
@@ -35,7 +34,7 @@ fact lsubv_inv_atom_sn_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L1 =
 #a #h #G #L1 #L2 * -L1 -L2
 [ //
 | #I #L1 #L2 #_ #H destruct
-| #L1 #L2 #W #V #_ #_ #_ #H destruct
+| #L1 #L2 #W #V #_ #_ #H destruct
 ]
 qed-.
 
@@ -46,20 +45,20 @@ lemma lsubv_inv_atom_sn (a) (h) (G): ∀L2. G ⊢ ⋆ ⫃![a,h] L2 → L2 = ⋆.
 fact lsubv_inv_bind_sn_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 →
                            ∀I,K1. L1 = K1.ⓘ{I} →
                            ∨∨ ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & L2 = K2.ⓘ{I}
-                            | ∃∃K2,W,V. ⦃G, K1⦄ ⊢ ⓝW.V ![a,h] & ⦃G, K2⦄ ⊢ W ![a,h] &
+                            | ∃∃K2,W,V. ⦃G, K1⦄ ⊢ ⓝW.V ![a,h] &
                                         G ⊢ K1 ⫃![a,h] K2 &
                                         I = BPair Abbr (ⓝW.V) & L2 = K2.ⓛW.
 #a #h #G #L1 #L2 * -L1 -L2
 [ #J #K1 #H destruct
 | #I #L1 #L2 #HL12 #J #K1 #H destruct /3 width=3 by ex2_intro, or_introl/
-| #L1 #L2 #W #V #HWV #HW #HL12 #J #K1 #H destruct /3 width=8 by ex5_3_intro, or_intror/
+| #L1 #L2 #W #V #HWV #HL12 #J #K1 #H destruct /3 width=7 by ex4_3_intro, or_intror/
 ]
 qed-.
 
 (* Basic_2A1: uses: lsubsv_inv_pair1 *)
 lemma lsubv_inv_bind_sn (a) (h) (G): ∀I,K1,L2. G ⊢ K1.ⓘ{I} ⫃![a,h] L2 →
                         ∨∨ ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & L2 = K2.ⓘ{I}
-                         | ∃∃K2,W,V. ⦃G, K1⦄ ⊢ ⓝW.V ![a,h] & ⦃G, K2⦄ ⊢ W ![a,h] &
+                         | ∃∃K2,W,V. ⦃G, K1⦄ ⊢ ⓝW.V ![a,h] &
                                      G ⊢ K1 ⫃![a,h] K2 &
                                      I = BPair Abbr (ⓝW.V) & L2 = K2.ⓛW.
 /2 width=3 by lsubv_inv_bind_sn_aux/ qed-.
@@ -68,7 +67,7 @@ fact lsubv_inv_atom_dx_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → L2 =
 #a #h #G #L1 #L2 * -L1 -L2
 [ //
 | #I #L1 #L2 #_ #H destruct
-| #L1 #L2 #W #V #_ #_ #_ #H destruct
+| #L1 #L2 #W #V #_ #_ #H destruct
 ]
 qed-.
 
@@ -79,22 +78,31 @@ lemma lsubv_inv_atom2 (a) (h) (G): ∀L1. G ⊢ L1 ⫃![a,h] ⋆ → L1 = ⋆.
 fact lsubv_inv_bind_dx_aux (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 →
                            ∀I,K2. L2 = K2.ⓘ{I} →
                            ∨∨ ∃∃K1. G ⊢ K1 ⫃![a,h] K2 & L1 = K1.ⓘ{I}
-                            | ∃∃K1,W,V. ⦃G, K1⦄ ⊢ ⓝW.V ![a,h] & ⦃G, K2⦄ ⊢ W ![a,h] &
+                            | ∃∃K1,W,V. ⦃G, K1⦄ ⊢ ⓝW.V ![a,h] &
                                         G ⊢ K1 ⫃![a,h] K2 & I = BPair Abst W & L1 = K1.ⓓⓝW.V.
 #a #h #G #L1 #L2 * -L1 -L2
 [ #J #K2 #H destruct
 | #I #L1 #L2 #HL12 #J #K2 #H destruct /3 width=3 by ex2_intro, or_introl/
-| #L1 #L2 #W #V #HWV #HW #HL12 #J #K2 #H destruct /3 width=8 by ex5_3_intro, or_intror/
+| #L1 #L2 #W #V #HWV #HL12 #J #K2 #H destruct /3 width=7 by ex4_3_intro, or_intror/
 ]
 qed-.
 
 (* Basic_2A1: uses: lsubsv_inv_pair2 *)
 lemma lsubv_inv_bind_dx (a) (h) (G): ∀I,L1,K2. G ⊢ L1 ⫃![a,h] K2.ⓘ{I} →
                         ∨∨ ∃∃K1. G ⊢ K1 ⫃![a,h] K2 & L1 = K1.ⓘ{I}
-                         | ∃∃K1,W,V. ⦃G, K1⦄ ⊢ ⓝW.V ![a,h] & ⦃G, K2⦄ ⊢ W ![a,h] &
+                         | ∃∃K1,W,V. ⦃G, K1⦄ ⊢ ⓝW.V ![a,h] &
                                      G ⊢ K1 ⫃![a,h] K2 & I = BPair Abst W & L1 = K1.ⓓⓝW.V.
 /2 width=3 by lsubv_inv_bind_dx_aux/ qed-.
 
+(* Advanced inversion lemmas ************************************************)
+
+lemma lsubv_inv_abst_sn (a) (h) (G): ∀K1,L2,W. G ⊢ K1.ⓛW ⫃![a,h] L2 →
+                        ∃∃K2. G ⊢ K1 ⫃![a,h] K2 & L2 = K2.ⓛW.
+#a #h #G #K1 #L2 #W #H
+elim (lsubv_inv_bind_sn … H) -H // *
+#K2 #XW #XV #_ #_ #H1 #H2 destruct
+qed-.
+
 (* Basic properties *********************************************************)
 
 (* Basic_2A1: uses: lsubsv_refl *)
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma
index 90b59cba0..06d302d57 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_drops.ma
@@ -34,7 +34,7 @@ lemma lsubv_drops_conf_isuni (a) (h) (G):
   | #g #Hg #HLK1 #H destruct -HL12
     elim (IH … Hg HLK1) -L1 -Hg /3 width=3 by drops_drop, ex2_intro/
   ]
-| #L1 #L2 #W #V #HVW #HW #HL12 #IH #b #f #K1 #Hf #H
+| #L1 #L2 #W #V #HVW #HL12 #IH #b #f #K1 #Hf #H
   elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
   [ #Hf #H destruct -IH
     /3 width=3 by drops_refl, lsubv_beta, ex2_intro/
@@ -59,7 +59,7 @@ lemma lsubv_drops_trans_isuni (a) (h) (G):
   | #g #Hg #HLK2 #H destruct -HL12
     elim (IH … Hg HLK2) -L2 -Hg /3 width=3 by drops_drop, ex2_intro/
   ]
-| #L1 #L2 #W #V #HWV #HW #HL12 #IH #b #f #K2 #Hf #H
+| #L1 #L2 #W #V #HWV #HL12 #IH #b #f #K2 #Hf #H
   elim (drops_inv_bind1_isuni … Hf H) -Hf -H *
   [ #Hf #H destruct -IH
     /3 width=3 by drops_refl, lsubv_beta, ex2_intro/
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsuba.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsuba.ma
index ac03aa297..daede63b3 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsuba.ma
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsuba.ma
@@ -22,7 +22,7 @@ include "basic_2/dynamic/lsubv.ma".
 (* Basic_2A1: uses: lsubsv_fwd_lsuba *)
 lemma lsubsv_fwd_lsuba (a) (h) (G): ∀L1,L2. G ⊢ L1 ⫃![a,h] L2 → G ⊢ L1 ⫃⁝ L2.
 #a #h #G #L1 #L2 #H elim H -L1 -L2 /2 width=1 by lsuba_bind/
-#L1 #L2 #W #V #H #_ #_ #IH
+#L1 #L2 #W #V #H #_ #IH
 elim (cnv_inv_cast … H) -H #W0 #HW #HV #HW0 #HVW0
 elim (cnv_fwd_aaa … HW) -HW #B #HW
 elim (cnv_fwd_aaa … HV) -HV #A #HV
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubv.ma b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubv.ma
new file mode 100644
index 000000000..d416b5f40
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/lsubv_lsubv.ma
@@ -0,0 +1,33 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "basic_2/dynamic/lsubv_cnv.ma".
+
+(* LOCAL ENVIRONMENT REFINEMENT FOR NATIVE VALIDITY *************************)
+
+(* Main properties **********************************************************)
+
+(* Note: not valid in Basic_2A1 *)
+theorem lsubv_trans (a) (h) (G): Transitive … (lsubv a h G).
+#a #h #G #L1 #L #H elim H -L1 -L //
+[ #I #K1 #K #HK1 #IH #Y #H
+  elim (lsubv_inv_bind_sn … H) -H *
+  [ #K2 #HK2 #H destruct /3 width=1 by lsubv_bind/
+  | #K2 #W #V #HWV #HK2 #H1 #H2 destruct /3 width=3 by lsubv_cnv_trans, lsubv_beta/
+  ]
+| #K1 #K #W #V #HWV #_ #IH #Y #H
+  elim (lsubv_inv_abst_sn … H) -H
+  #K2 #HK2 #H1 destruct /3 width=1 by lsubv_beta/
+]
+qed-.
diff --git a/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt b/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt
index ad9b95be0..361be816f 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt
+++ b/matita/matita/contribs/lambdadelta/basic_2/dynamic/partial.txt
@@ -1,3 +1,3 @@
 cnv.ma cnv_drops.ma cnv_fqus.ma cnv_aaa.ma cnv_fsb.ma
 cnv_etc.ma cnv_cpm_trans.ma
-lsubv.ma lsubv_drops.ma lsubv_lsubr.ma lsubv_lsuba.ma lsubv_cpms.ma lsubv_cpcs.ma lsubv_cnv.ma
+lsubv.ma lsubv_drops.ma lsubv_lsubr.ma lsubv_lsuba.ma lsubv_cpms.ma lsubv_cpcs.ma lsubv_cnv.ma lsubv_lsubv.ma
diff --git a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
index 1c19f4e3a..32063da4b 100644
--- a/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
+++ b/matita/matita/contribs/lambdadelta/basic_2/web/basic_2_src.tbl
@@ -30,8 +30,8 @@ table {
         ]
 *)
         [ { "context-sensitive native validity" * } {
-             [ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" * ]
-             [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "snv_cpm_trans" (* + "snv_scpes" + "snv_preserve" *) * ]
+             [ [ "restricted refinement for lenvs" ] "lsubv ( ? ⊢ ? ⫃![?,?] ? )" "lsubv_drops" + "lsubv_lsubr" + "lsubv_lsuba" + "lsubv_cpms" + "lsubv_cpcs" + "lsubv_cnv" + "lsubv_lsubv" * ]
+             [ [ "for terms" ] "cnv" + "( ⦃?,?⦄ ⊢ ? ![?,?] )" "cnv_drops" + "cnv_fqus" + "cnv_aaa" + "cnv_fsb" + "cnv_cpm_trans" (* + "cnv_scpes" + "cnv_preserve" *) * ]
           }
         ]
      }
diff --git a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
index 932f95de2..e3ec5c504 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/lib/arith.ma
@@ -147,6 +147,9 @@ fact le_repl_sn_trans_aux: ∀x,y,z:nat. x ≤ z → y = x → y ≤ z.
 lemma monotonic_le_minus_l2: ∀x1,x2,y,z. x1 ≤ x2 → x1 - y - z ≤ x2 - y - z.
 /3 width=1 by monotonic_le_minus_l/ qed.
 
+lemma minus_le_trans_sn: ∀x1,x2. x1 ≤ x2 → ∀x. x1-x ≤ x2.
+/2 width=3 by transitive_le/ qed.
+
 (* Note: this might interfere with nat.ma *)
 lemma monotonic_lt_pred: ∀m,n. m < n → 0 < m → pred m < pred n.
 #m #n #Hmn #Hm whd >(S_pred … Hm)