]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/arith/nat_le_max.ma
update in delayed_updating
[helm.git] / 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_2_succ … 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 // qed.
39
40 (* Basic destructions with nmax *********************************************)
41
42 (*** le_maxl *)
43 lemma nle_des_max_sn_sn (m1) (m2) (n): (m1 ∨ m2) ≤ n → m1 ≤ n.
44 /2 width=3 by nle_trans/ qed-.
45
46 (*** le_maxr *)
47 lemma nle_des_max_sn_dx (m1) (m2) (n): (m1 ∨ m2) ≤ n → m2 ≤ n.
48 /2 width=3 by nle_trans/ qed-.
49
50 (* Advanced constructions with nmax *****************************************)
51
52 (*** max_S1_le_S *)
53 lemma nle_max_sn_succ_sn (m1) (m2) (n): (m1 ∨ m2) ≤ n → (↑m1 ∨ m2) ≤ ↑n.
54 /4 width=2 by nle_des_max_sn_sn, nle_des_max_sn_dx, nle_max_sn, nle_succ_bi, nle_succ_dx/ qed.
55
56 (*** max_S2_le_S *)
57 lemma nle_max_sn_succ_dx (m1) (m2) (n): (m1 ∨ m2) ≤ n → (m1 ∨ ↑m2) ≤ ↑n.
58 /4 width=2 by nle_des_max_sn_sn, nle_des_max_sn_dx, nle_max_sn, nle_succ_bi, nle_succ_dx/ qed.