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 (* NON-NEGATIVE INTEGERS ****************************************************)
  19
  20 (* Basic constructions with plus ********************************************)
  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_b *)
  42 lemma nle_plus_dx_dx (m) (n) (o): n + o ≤ m → n ≤ m.
  43 /2 width=3 by nle_trans/ qed.
  44
  45 (*** le_plus_a *)
  46 lemma nle_plus_dx_sn (m) (n) (o): n ≤ m → n ≤ o + m.
  47 /2 width=3 by nle_trans/ qed.
  48
  49 (* Main constructions with plus *********************************************)
  50
  51 (*** le_plus *)
  52 theorem nle_plus_bi (m1) (m2) (n1) (n2):
  53         m1 ≤ m2 → n1 ≤ n2 → m1 + n1 ≤ m2 + n2.
  54 /3 width=3 by nle_plus_bi_dx, nle_plus_bi_sn, nle_trans/ qed.
  55
  56 (* Basic inversions with plus ***********************************************)
  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_nzero_plus/ 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 … 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