matita/matita/contribs/lambdadelta/ground/arith/ynat_le_minus1.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_minus.ma".
  16 include "ground/arith/ynat_minus1.ma".
  17 include "ground/arith/ynat_le.ma".
  18
  19 (* ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY ****************************)
  20
  21 (* Constructions with yminus1 ***********************************************)
  22
  23 (*** yle_minus_sn *)
  24 lemma yle_minus1_sn_refl_sn (x) (n): x - n ≤ x.
  25 #x @(ynat_split_nat_inf … x) -x //
  26 #m #n /2 width=1 by yle_inj/
  27 qed.
  28
  29 (*** monotonic_yle_minus_dx *)
  30 lemma yle_minus1_bi_dx (o) (x) (y):
  31       x ≤ y → x - o ≤ y - o.
  32 #o #x #y *
  33 /3 width=1 by nle_minus_bi_dx, yle_inj, yle_inf/
  34 qed.
  35
  36 (*** yminus_to_le *)
  37 lemma yle_eq_zero_minus1 (x) (n): 𝟎 = x - n → x ≤ yinj_nat n.
  38 #x @(ynat_split_nat_inf … x) -x
  39 [ #m #n <yminus1_inj_sn >yinj_nat_zero #H
  40   /4 width=1 by nle_eq_zero_minus, yle_inj, eq_inv_yinj_nat_bi/
  41 | #n <yminus1_inf_sn #H destruct
  42 ]
  43 qed.
  44
  45 (* Inversions with yminus1 **************************************************)
  46
  47 (*** yle_to_minus *)
  48 lemma yle_inv_eq_zero_minus1 (x) (n):
  49       x ≤ yinj_nat n → 𝟎 = x - n.
  50 #x @(ynat_split_nat_inf … x) -x
  51 [ #m #n #H <yminus1_inj_sn
  52   /4 width=1 by nle_inv_eq_zero_minus, yle_inv_inj_bi, eq_f/
  53 | #n #H
  54   lapply (yle_inv_inf_sn … H) -H #H
  55   elim (eq_inv_inf_yinj_nat … H)
  56 ]
  57 qed-.