matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "ground/generated/pull_2.ma".
  16 include "ground/arith/nat_le_minus.ma".
  17 include "ground/arith/nat_lt_pred.ma".
  18
  19 (* STRICT ORDER FOR NON-NEGATIVE INTEGERS ***********************************)
  20
  21 (* Constructions with nminus ************************************************)
  22
  23 (*** monotonic_lt_minus_l *)
  24 lemma nlt_minus_bi_dx (o) (m) (n): o ≤ m → m < n → m - o < n - o.
  25 #o #m #n #Hom #Hmn
  26 lapply (nle_minus_bi_dx … o Hmn) -Hmn
  27 <(nminus_succ_sn … Hom) //
  28 qed.
  29
  30 (*** monotonic_lt_minus_r *)
  31 lemma nlt_minus_bi_sn (o) (m) (n):
  32       m < o -> m < n → o-n < o-m.
  33 #o #m #n #Ho #H
  34 lapply (nle_minus_bi_sn … o H) -H #H
  35 @(nle_nlt_trans … H) -n
  36 @nlt_i >(nminus_succ_sn … Ho) //
  37 qed.
  38
  39 (* Inversions with nminus ***************************************************)
  40
  41 lemma nlt_inv_minus_bi_dx (o) (m) (n):
  42       m - o < n - o → m < n.
  43 #o @(nat_ind_succ … o) -o
  44 /3 width=1 by nlt_inv_pred_bi/
  45 qed-.
  46
  47 (* Destructions with nminus *************************************************)
  48
  49 (*** minus_pred_pred *)
  50 lemma nminus_pred_bi (m) (n): 𝟎 < m → 𝟎 < n → n - m = ↓n - ↓m.
  51 #m #n #Hm #Hn
  52 >(nlt_des_gen … Hm) in ⊢ (??%?); -Hm
  53 >(nlt_des_gen … Hn) in ⊢ (??%?); -Hn
  54 //
  55 qed-.
  56
  57 lemma nlt_des_minus_dx (o) (m) (n): m < n - o → o < n.
  58 #o @(nat_ind_succ … o) -o
  59 [ #m #n <nminus_zero_dx
  60   /2 width=3 by nle_nlt_trans/
  61 | #o #IH #m #n <nminus_succ_dx_pred_sn #H
  62   /3 width=2 by nlt_inv_pred_dx/
  63 ]
  64 qed-.
  65
  66 (* Advanced eliminators for nle with nlt and nminus *************************)
  67
  68 (*** nat_elim_le_sn *)
  69 lemma nle_ind_sn (Q:relation …):
  70       (∀m1,m2. (∀m. m < m2-m1 → Q (m2-m) m2) → m1 ≤ m2 → Q m1 m2) →
  71       ∀n1,n2. n1 ≤ n2 → Q n1 n2.
  72 #Q #IH #n1 #n2 #Hn
  73 >(nminus_minus_dx_refl_sn … Hn) -Hn
  74 lapply (nle_minus_sn_refl_sn n2 n1)
  75 let d ≝ (n2-n1)
  76 @(nat_ind_lt … d) -d -n1 #d
  77 @pull_2 #Hd
  78 >(nminus_minus_dx_refl_sn … Hd) in ⊢ (%→?); -Hd
  79 let n1 ≝ (n2-d) #IHd
  80 @IH -IH [| // ] #m #Hn
  81 /4 width=3 by nlt_des_le, nlt_nle_trans/
  82 qed-.