matita/matita/contribs/lambdadelta/ground/arith/ynat_lt_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_lt_plus.ma".
  16 include "ground/arith/ynat_plus.ma".
  17 include "ground/arith/ynat_lt_succ.ma".
  18
  19 (* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
  20
  21 (* Constructions with yplus *************************************************)
  22
  23 (*** ylt_plus_Y *)
  24 lemma ylt_plus_inf (x) (y):
  25       x < ∞ → y < ∞ → x + y < ∞.
  26 #x #y #Hx #Hy
  27 elim (ylt_des_gen_sn … Hx) -Hx #m #H destruct
  28 elim (ylt_des_gen_sn … Hy) -Hy #n #H destruct
  29 //
  30 qed.
  31
  32 (*** ylt_plus_dx1_trans *)
  33 lemma ylt_plus_dx_sn (z) (x) (y):
  34       z < x → z < x + y.
  35 #z #x #y * -z -x //
  36 #o #m #Hom @(ynat_split_nat_inf … y) - y //
  37 /3 width=1 by ylt_inj, nle_plus_bi/
  38 qed.
  39
  40 (*** ylt_plus_dx2_trans *)
  41 lemma ylt_plus_dx_dx (z) (x) (y):
  42       z < y → z < x + y.
  43 #z #x #y <yplus_comm
  44 /2 width=1 by ylt_plus_dx_sn/
  45 qed.
  46
  47 (*** monotonic_ylt_plus_dx_inj *)
  48 lemma ylt_plus_bi_dx_inj (o) (x) (y):
  49       x < y → x + yinj_nat o < y + yinj_nat o.
  50 #o #x #y #Hxy
  51 @(nat_ind_succ … o) -o //
  52 #n #IH >ysucc_inj <yplus_succ_dx <yplus_succ_dx
  53 /2 width=1 by ylt_succ_bi/
  54 qed.
  55
  56 (*** monotonic_ylt_plus_sn_inj *)
  57 lemma ylt_plus_bi_sn_inj (o) (x) (y):
  58       x < y → yinj_nat o + x < yinj_nat o + y.
  59 /2 width=1 by ylt_plus_bi_dx_inj/ qed.
  60
  61 (*** monotonic_ylt_plus_dx *)
  62 lemma ylt_plus_bi_dx (z) (x) (y):
  63       x < y → z < ∞ → x + z < y + z.
  64 #z #x #y #Hxy #Hz
  65 elim (ylt_des_gen_sn … Hz) -Hz #o #H destruct
  66 /2 width=1 by ylt_plus_bi_dx_inj/
  67 qed.
  68
  69 (*** monotonic_ylt_plus_sn *)
  70 lemma ylt_plus_bi_sn (z) (x) (y):
  71       x < y → z < ∞ → z + x < z + y.
  72 #z #x #y #Hxy #Hz <yplus_comm <yplus_comm in ⊢ (??%);
  73 /2 width=1 by ylt_plus_bi_dx/
  74 qed.
  75
  76 (* Inversions with yplus ****************************************************)
  77
  78 (*** yplus_inv_monotonic_dx *)
  79 lemma eq_inv_yplus_bi_dx (z) (x) (y):
  80       z < ∞ → x + z = y + z → x = y.
  81 #z #x #y #H
  82 elim (ylt_des_gen_sn … H) -H #o #H destruct
  83 /2 width=2 by eq_inv_yplus_bi_dx_inj/
  84 qed-.
  85
  86 (*** yplus_inv_monotonic_23 *)
  87 lemma yplus_inv_plus_bi_23 (z) (x1) (x2) (y1) (y2):
  88       z < ∞ → x1 + z + y1 = x2 + z + y2 → x1 + y1 = x2 + y2.
  89 #z #x1 #x2 #y1 #y2 #Hz
  90 <yplus_plus_comm_23 <yplus_plus_comm_23 in ⊢ (???%→?); #H
  91 @(eq_inv_yplus_bi_dx … H) // (* * auto does not work *)
  92 qed-.
  93
  94 (*** ylt_inv_plus_Y *)
  95 lemma ylt_inv_plus_inf (x) (y):
  96       x + y < ∞ → ∧∧ x < ∞ & y < ∞.
  97 #x #y #H
  98 elim (ylt_des_gen_sn … H) -H #o #H
  99 elim (eq_inv_yplus_inj … H) -H
 100 /2 width=1 by conj/
 101 qed-.
 102
 103 (* Destructions with yplus **************************************************)
 104
 105 (*** ylt_inv_monotonic_plus_dx *)
 106 lemma ylt_des_plus_bi_dx (z) (x) (y):
 107       x + z < y + z → x < y.
 108 #z @(ynat_split_nat_inf … z) -z
 109 [ #o #x @(ynat_split_nat_inf … x) -x
 110   [ #m #y @(ynat_split_nat_inf … y) -y //
 111     #n <yplus_inj_bi <yplus_inj_bi #H
 112     /4 width=2 by ylt_inv_inj_bi, ylt_inj, nlt_inv_plus_bi_dx/
 113   | #y <yplus_inf_sn #H
 114     elim (ylt_inv_inf_sn … H)
 115   ]
 116 | #x #y <yplus_inf_dx #H
 117   elim (ylt_inv_inf_sn … H)
 118 ]
 119 qed-.
 120
 121 lemma ylt_des_plus_bi_sn (z) (x) (y):
 122       z + x < z + y → x < y.
 123 /2 width=2 by ylt_des_plus_bi_dx/ qed-.