matita/matita/contribs/lambdadelta/ground/arith/nat_le_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_plus.ma".
  16 include "ground/arith/nat_le.ma".
  17
  18 (* ORDER FOR NON-NEGATIVE INTEGERS ****************************************************)
  19
  20 (* Constructions with nplus ***********************************************************)
  21
  22 (*** monotonic_le_plus_l *)
  23 lemma nle_plus_bi_dx (m) (n1) (n2): n1 ≤ n2 → n1 + m ≤ n2 + m.
  24 #m #n1 #n2 #H elim H -n2 /2 width=3 by nle_trans/
  25 qed.
  26
  27 (*** monotonic_le_plus_r *)
  28 lemma nle_plus_bi_sn (m) (n1) (n2): n1 ≤ n2 → m + n1 ≤ m + n2.
  29 #m #n1 #n2 #H <nplus_comm <nplus_comm in ⊢ (??%);
  30 /2 width=1 by nle_plus_bi_dx/
  31 qed.
  32
  33 (*** le_plus_n_r *)
  34 lemma nle_plus_dx_dx_refl (m) (n): m ≤ m + n.
  35 /2 width=1 by nle_plus_bi_sn/ qed.
  36
  37 (*** le_plus_n *)
  38 lemma nle_plus_dx_sn_refl (m) (n): m ≤ n + m.
  39 /2 width=1 by nle_plus_bi_sn/ qed.
  40
  41 (*** le_plus_a *)
  42 lemma nle_plus_dx_sn (m) (n) (o): n ≤ m → n ≤ o + m.
  43 /2 width=3 by nle_trans/ qed.
  44
  45 (* Main constructions with nplus ********************************************)
  46
  47 (*** le_plus *)
  48 theorem nle_plus_bi (m1) (m2) (n1) (n2):
  49         m1 ≤ m2 → n1 ≤ n2 → m1 + n1 ≤ m2 + n2.
  50 /3 width=3 by nle_plus_bi_dx, nle_plus_bi_sn, nle_trans/ qed.
  51
  52 (* Inversions with nplus ****************************************************)
  53
  54 (*** le_plus_b *)
  55 lemma nle_inv_plus_sn_dx (m) (n) (o): n + o ≤ m → n ≤ m.
  56 /2 width=3 by nle_trans/ qed.
  57
  58 (*** plus_le_0 *)
  59 lemma nle_inv_plus_zero (m) (n): m + n ≤ 𝟎 → ∧∧ 𝟎 = m & 𝟎 = n.
  60 /3 width=1 by nle_inv_zero_dx, eq_inv_zero_nplus/ qed-.
  61
  62 (*** le_plus_to_le_r *)
  63 lemma nle_inv_plus_bi_dx (o) (m) (n): n + o ≤ m + o → n ≤ m.
  64 #o @(nat_ind_succ … o) -o /3 width=1 by nle_inv_succ_bi/
  65 qed-.
  66
  67 (*** le_plus_to_le *)
  68 lemma nle_inv_plus_bi_sn (o) (m) (n): o + n ≤ o + m → n ≤ m.
  69 /2 width=2 by nle_inv_plus_bi_dx/ qed-.
  70
  71 (* Destructions with nplus **************************************************)
  72
  73 (*** plus2_le_sn_sn *)
  74 lemma nplus_2_des_le_sn_sn (m1) (m2) (n1) (n2):
  75       m1 + n1 = m2 + n2 → m1 ≤ m2 → n2 ≤ n1.
  76 #m1 #m2 #n1 #n2 #H #Hm
  77 lapply (nle_plus_bi_dx n1 … Hm) -Hm >H -H
  78 /2 width=2 by nle_inv_plus_bi_sn/
  79 qed-.
  80
  81 (*** plus2_le_sn_dx *)
  82 lemma nplus_2_des_le_sn_dx (m1) (m2) (n1) (n2):
  83       m1 + n1 = n2 + m2 → m1 ≤ m2 → n2 ≤ n1.
  84 #m1 #m2 #n1 #n2 <nplus_comm in ⊢ (???%→?);
  85 /2 width=4 by nplus_2_des_le_sn_sn/ qed-.
  86
  87 (*** plus2_le_dx_sn *)
  88 lemma nplus_2_des_le_dx_sn (m1) (m2) (n1) (n2):
  89       n1 + m1 = m2 + n2 → m1 ≤ m2 → n2 ≤ n1.
  90 #m1 #m2 #n1 #n2 <nplus_comm in ⊢ (??%?→?);
  91 /2 width=4 by nplus_2_des_le_sn_sn/ qed-.
  92
  93 (*** plus2_le_dx_dx *)
  94 lemma nplus_2_des_le_dx_dx (m1) (m2) (n1) (n2):
  95       n1 + m1 = n2 + m2 → m1 ≤ m2 → n2 ≤ n1.
  96 #m1 #m2 #n1 #n2 <nplus_comm in ⊢ (??%?→?);
  97 /2 width=4 by nplus_2_des_le_sn_dx/ qed-.