]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/lambdadelta/ground/arith/nat_lt_minus.ma
update in delayed_updating
[helm.git] / matita / matita / contribs / lambdadelta / ground / arith / nat_lt_minus.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/generated/pull_2.ma".
16 include "ground/arith/nat_le_minus.ma".
17 include "ground/arith/nat_lt_pred.ma".
18
19 (* STRICT ORDER FOR NON-NEGATIVE INTEGERS ***********************************)
20
21 (* Constructions with nminus ************************************************)
22
23 (*** monotonic_lt_minus_l *)
24 lemma nlt_minus_bi_dx (o) (m) (n): o ≤ m → m < n → m - o < n - o.
25 #o #m #n #Hom #Hmn
26 lapply (nle_minus_bi_dx … o Hmn) -Hmn
27 <(nminus_succ_sn … Hom) //
28 qed.
29
30 (*** monotonic_lt_minus_r *)
31 lemma nlt_minus_bi_sn (o) (m) (n):
32       m < o -> m < n → o-n < o-m.
33 #o #m #n #Ho #H
34 lapply (nle_minus_bi_sn … o H) -H #H
35 @(nle_nlt_trans … H) -n
36 @nlt_i >(nminus_succ_sn … Ho) //
37 qed.
38
39 (* Inversions with nminus ***************************************************)
40
41 lemma nlt_inv_minus_bi_dx (o) (m) (n):
42       m - o < n - o → m < n.
43 #o @(nat_ind_succ … o) -o
44 /3 width=1 by nlt_inv_pred_bi/
45 qed-.
46
47 (* Destructions with nminus *************************************************)
48
49 (*** minus_pred_pred *)
50 lemma nminus_pred_bi (m) (n): 𝟎 < m → 𝟎 < n → n - m = ↓n - ↓m.
51 #m #n #Hm #Hn
52 >(nlt_des_gen … Hm) in ⊢ (??%?); -Hm
53 >(nlt_des_gen … Hn) in ⊢ (??%?); -Hn
54 //
55 qed-.
56
57 lemma nlt_des_minus_dx (o) (m) (n): m < n - o → o < n.
58 #o @(nat_ind_succ … o) -o
59 [ #m #n <nminus_zero_dx
60   /2 width=3 by nle_nlt_trans/
61 | #o #IH #m #n <nminus_succ_dx_pred_sn #H
62   /3 width=2 by nlt_inv_pred_dx/
63 ]
64 qed-.
65
66 (* Advanced eliminators for nle with nlt and nminus *************************)
67
68 (*** nat_elim_le_sn *)
69 lemma nle_ind_sn (Q:relation …):
70       (∀m1,m2. (∀m. m < m2-m1 → Q (m2-m) m2) → m1 ≤ m2 → Q m1 m2) →
71       ∀n1,n2. n1 ≤ n2 → Q n1 n2.
72 #Q #IH #n1 #n2 #Hn
73 >(nminus_minus_dx_refl_sn … Hn) -Hn
74 lapply (nle_minus_sn_refl_sn n2 n1)
75 let d ≝ (n2-n1)
76 @(nat_ind_lt … d) -d -n1 #d
77 @pull_2 #Hd
78 >(nminus_minus_dx_refl_sn … Hd) in ⊢ (%→?); -Hd
79 let n1 ≝ (n2-d) #IHd
80 @IH -IH [| // ] #m #Hn
81 /4 width=3 by nlt_des_le, nlt_nle_trans/
82 qed-.