matita/matita/contribs/lambdadelta/ground/arith/nat_le_minus_plus.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/arith/nat_minus_plus.ma".
  16 include "ground/arith/nat_le_plus.ma".
  17 include "ground/arith/nat_le_minus.ma".
  18
  19 (* ORDER FOR NON-NEGATIVE INTEGERS ******************************************)
  20
  21 (* Constructions with nminus and nplus **************************************)
  22
  23 (*** le_plus_minus_m_m *)
  24 lemma nle_plus_minus_sn_refl_sn (n) (m): m ≤ m - n + n.
  25 #n @(nat_ind_succ … n) -n //
  26 #n #IH #m <nminus_succ_dx_pred_sn <nplus_succ_dx
  27 /2 width=1 by nle_inv_pred_sn/
  28 qed.
  29
  30 lemma plus_minus_sn_refl_sn_nle (m) (n): n = n - m + m → m ≤ n.
  31 // qed.
  32
  33 (*** le_plus_to_minus *)
  34 lemma nle_minus_sn (o) (m) (n): m ≤ n + o → m - o ≤ n.
  35 /2 width=1 by nle_minus_sn_bi/ qed.
  36
  37 (*** le_plus_to_minus_r *)
  38 lemma nle_minus_dx (o) (m) (n): m + o ≤ n → m ≤ n - o.
  39 #o #m #n #H >(nminus_plus_sn_refl_sn m o)
  40 /2 width=1 by nle_minus_sn_bi/
  41 qed.
  42
  43 (*** le_inv_plus_l *)
  44 lemma nle_minus_dx_full (o) (m) (n): m + o ≤ n → ∧∧ m ≤ n - o & o ≤ n.
  45 /3 width=3 by nle_minus_dx, nle_trans, conj/ qed-.
  46
  47 (* Inversions with nminus and nplus *****************************************)
  48
  49 (*** plus_minus_m_m *)
  50 lemma nplus_minus_sn_refl_sn (m) (n): m ≤ n → n = n - m + m.
  51 #m #n #H elim H -n //
  52 #n #Hn #IH <(nminus_succ_sn … Hn) -Hn
  53 <nplus_succ_sn //
  54 qed-.
  55
  56 lemma nplus_minus_dx_refl_sn (m) (n): m ≤ n → n = m + (n - m).
  57 #m #n <nplus_comm
  58 /2 width=1 by nplus_minus_sn_refl_sn/
  59 qed-.
  60
  61 (*** le_minus_to_plus *)
  62 lemma nle_inv_minus_sn (o) (m) (n): m - o ≤ n → m ≤ n + o.
  63 /3 width=3 by nle_plus_bi_dx, nle_trans/ qed-.
  64
  65 (*** le_minus_to_plus_r *)
  66 lemma nle_inv_minus_dx (o) (m) (n): o ≤ n → m ≤ n - o → m + o ≤ n.
  67 #o #m #n #Hon #Hm
  68 >(nplus_minus_sn_refl_sn … Hon)
  69 /2 width=1 by nle_plus_bi_dx/
  70 qed-.
  71
  72 (* Destructions with nminus and nplus ***************************************)
  73
  74 (*** plus_minus *)
  75 lemma nminus_plus_comm_23 (o) (m) (n):
  76       m ≤ n → n - m + o = n + o - m.
  77 #o #m #n #H elim H -n //
  78 #n #Hn #IH <(nminus_succ_sn … Hn)
  79 <nplus_succ_sn <nplus_succ_sn <nminus_succ_sn //
  80 /2 width=3 by nle_trans/
  81 qed-.
  82
  83 (*** plus_minus_associative *)
  84 lemma nplus_minus_assoc (m1) (m2) (n):
  85       n ≤ m2 → m1 + m2 - n = m1 + (m2 - n).
  86 /2 width=1 by nminus_plus_comm_23/ qed-.
  87
  88 (*** minus_minus_associative *)
  89 theorem nminus_assoc (m1) (m2) (m3):
  90         m3 ≤ m2 → m2 ≤ m1 → m1 - m2 + m3 = m1 - (m2 - m3).
  91 #m1 #m2 #m3 #Hm32 #Hm21
  92 @nminus_plus_sn >nplus_assoc
  93 <nplus_minus_dx_refl_sn //
  94 /2 width=1 by nplus_minus_sn_refl_sn/
  95 qed-.
  96
  97 (*** minus_minus *)
  98 theorem nminus_assoc_comm (m1) (m2) (m3):
  99         m3 ≤ m2 → m2 ≤ m1 → m3 + (m1 - m2) = m1 - (m2 - m3).
 100 #m1 #m2 #m3 #Hm32 #Hm21 <nplus_comm
 101 /2 width=1 by nminus_assoc/
 102 qed-.
 103
 104 (*** minus_le_minus_minus_comm *)
 105 theorem minus_assoc_comm_23 (m1) (m2) (m3):
 106         m3 ≤ m2 → m1 + m3 - m2 = m1 - (m2 - m3).
 107 #m1 #m2 #m3 #Hm
 108 >(nplus_minus_sn_refl_sn … Hm) in ⊢ (??%?); //
 109 qed-.