matita/matita/contribs/lambdadelta/ground/arith/nat_le_max.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_max.ma".
  16 include "ground/arith/nat_le.ma".
  17
  18 (* ORDER FOR NON-NEGATIVE INTEGERS ******************************************)
  19
  20 (* Basic constructions with nmax ********************************************)
  21
  22 (*** to_max *)
  23 lemma nle_max_sn (n):
  24       ∀m1. m1 ≤ n → ∀m2. m2 ≤ n → (m1 ∨ m2) ≤ n.
  25 #n #m1 #H @(nle_ind_alt … H) -n -m1 //
  26 #n #m1 #Hnm1 #IH #m2 @(nat_ind_succ … m2) -m2
  27 [ #_ -IH /3 width=1 by nle_succ_bi/
  28 | #m2 #_ #H -Hnm1 /4 width=1 by nle_inv_succ_bi, nle_succ_bi/
  29 ]
  30 qed.
  31
  32 lemma nle_max_dx_refl_sn (m) (n): m ≤ (m ∨ n).
  33 #m #n @(nat_ind_succ_2 … m n) -m -n //
  34 #m #n #IH <nmax_succ_bi /2 width=1 by nle_succ_bi/
  35 qed.
  36
  37 lemma nle_max_dx_refl_dx (m) (n): n ≤ (m ∨ n).
  38 #m #n @(nat_ind_succ_2 … n m) -m -n //
  39 #m #n #IH <nmax_succ_bi /2 width=1 by nle_succ_bi/
  40 qed.
  41
  42 (* Basic destructions with nmax *********************************************)
  43
  44 (*** le_maxl *)
  45 lemma nle_des_max_sn_sn (m1) (m2) (n): (m1 ∨ m2) ≤ n → m1 ≤ n.
  46 /2 width=3 by nle_trans/ qed-.
  47
  48 (*** le_maxr *)
  49 lemma nle_des_max_sn_dx (m1) (m2) (n): (m1 ∨ m2) ≤ n → m2 ≤ n.
  50 /2 width=3 by nle_trans/ qed-.
  51
  52 (* Advanced constructions with nmax *****************************************)
  53
  54 (*** max_S1_le_S *)
  55 lemma nle_max_sn_succ_sn (m1) (m2) (n): (m1 ∨ m2) ≤ n → (↑m1 ∨ m2) ≤ ↑n.
  56 /4 width=2 by nle_des_max_sn_sn, nle_des_max_sn_dx, nle_max_sn, nle_succ_bi, nle_succ_dx/ qed.
  57
  58 (*** max_S2_le_S *)
  59 lemma nle_max_sn_succ_dx (m1) (m2) (n): (m1 ∨ m2) ≤ n → (m1 ∨ ↑m2) ≤ ↑n.
  60 /4 width=2 by nle_des_max_sn_sn, nle_des_max_sn_dx, nle_max_sn, nle_succ_bi, nle_succ_dx/ qed.