matita/matita/contribs/lambdadelta/ground/arith/ynat_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_le_plus.ma".
  16 include "ground/arith/ynat_plus.ma".
  17 include "ground/arith/ynat_le_succ.ma".
  18
  19 (* ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY ****************************)
  20
  21 (* Constructions with yplus *************************************************)
  22
  23 (*** monotonic_yle_plus *)
  24 lemma yle_plus_bi (x1) (x2) (y1) (y2):
  25       x1 ≤ y1 → x2 ≤ y2 → x1 + x2 ≤ y1 + y2.
  26 #x1 #x2 #y1 #y2 * //
  27 #m1 #n1 #Hmn1 * //
  28 #m2 #n2 #Hmn2 /3 width=1 by nle_plus_bi, yle_inj/
  29 qed.
  30
  31 (*** monotonic_yle_plus_dx *)
  32 lemma yle_plus_bi_dx (z) (x) (y):
  33       x ≤ y → x + z ≤ y + z.
  34 /2 width=1 by yle_plus_bi/ qed.
  35
  36 (*** monotonic_yle_plus_sn *)
  37 lemma yle_plus_bi_sn (z) (x) (y):
  38       x ≤ y → z + x ≤ z + y.
  39 /2 width=1 by yle_plus_bi/ qed.
  40
  41 (*** yle_plus_dx1_trans *)
  42 lemma yle_plus_dx_dx (z) (x) (y):
  43       z ≤ x → z ≤ x + y.
  44 /2 width=1 by yle_plus_bi/ qed.
  45
  46 (*** yle_plus_dx2_trans *)
  47 lemma yle_plus_dx_sn (z) (x) (y):
  48       z ≤ y → z ≤ x + y.
  49 #z #x #y <yplus_comm
  50 /2 width=3 by yle_plus_dx_dx/
  51 qed.
  52
  53 (*** yle_plus_dx1 *)
  54 lemma yle_plus_dx_dx_refl (x) (y): x ≤ x + y.
  55 /2 width=1 by yle_plus_dx_dx/ qed.
  56
  57 (*** yle_plus_dx2 *)
  58 lemma yle_plus_dx_sn_refl (x) (y): y ≤ x + y.
  59 // qed-.
  60
  61 (* Inversions with yplus ****************************************************)
  62
  63 (*** yle_inv_monotonic_plus_dx_inj *)
  64 lemma yle_inv_plus_bi_dx_inj (o) (x) (y):
  65       x + yinj_nat o ≤ y + yinj_nat o → x ≤ y.
  66 #o @(nat_ind_succ … o) -o //
  67 #o #IH #x #y >ysucc_inj <yplus_succ_dx <yplus_succ_dx #H
  68 /3 width=1 by yle_inv_succ_bi/
  69 qed-.
  70
  71 (*** yle_inv_monotonic_plus_sn_inj *)
  72 lemma yle_inv_plus_bi_sn_inj (o) (x) (y):
  73       yinj_nat o + x ≤ yinj_nat o + y → x ≤ y.
  74 /2 width=2 by yle_inv_plus_bi_dx_inj/ qed-.
  75
  76 (* Destructions with yplus **************************************************)
  77
  78 (*** yle_fwd_plus_sn2 *)
  79 lemma yle_des_plus_sn_sn (x) (y) (z):
  80       x + y ≤ z → y ≤ z.
  81 /2 width=3 by yle_trans/ qed-.
  82
  83 (*** yle_fwd_plus_sn1 *)
  84 lemma yle_des_plus_sn_dx (x) (y) (z):
  85       x + y ≤ z → x ≤ z.
  86 /2 width=3 by yle_trans/ qed-.
  87
  88 (*** yle_fwd_plus_ge *)
  89 lemma yle_des_plus_bi_sn_inj_bi (m) (n) (x) (y):
  90       n ≤ m → yinj_nat m + x ≤ yinj_nat n + y → x ≤ y.
  91 #m #n #x #y #Hnm #H
  92 lapply (yle_inj … Hnm) -Hnm #Hnm
  93 lapply (yle_plus_bi … Hnm … H) -Hnm -H
  94 <yplus_assoc <yplus_inj_bi <yplus_assoc <yplus_inj_bi #H
  95 /2 width=2 by yle_inv_plus_bi_sn_inj/
  96 qed-.
  97
  98 (*** yle_fwd_plus_ge_inj *)
  99 lemma yle_des_plus_bi_sn_inj_sn (o) (z) (x) (y):
 100       z ≤ yinj_nat o → yinj_nat o + x ≤ z + y → x ≤ y.
 101 #m #z #x #y #H elim (yle_inv_inj_dx … H) -H
 102 #n #Hnm #H destruct
 103 /2 width=4 by yle_des_plus_bi_sn_inj_bi/
 104 qed-.
 105
 106 (*** yle_fwd_plus_yge *)
 107 lemma yle_des_plus_bi_sn_inj_md (m1) (m2) (y1) (y2):
 108       yinj_nat m2 ≤ y1 → y1 + yinj_nat m1 ≤ yinj_nat m2 + y2 → yinj_nat m1 ≤ y2.
 109 #m1 #m2 #y1 #y2 @(ynat_split_nat_inf … y2) -y2 //
 110 #n2 @(ynat_split_nat_inf … y1) -y1
 111 /2 width=4 by yle_des_plus_bi_sn_inj_sn/
 112 qed-.