1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 include "ground/arith/ynat_le.ma".
16 include "ground/arith/ynat_lt.ma".
18 (* STRICT ORDER FOR NON-NEGATIVE INTEGERS WITH INFINITY *********************)
20 (* Constructions with yle ***************************************************)
23 lemma yle_split_lt_eq (x) (y):
24 x ≤ y → ∨∨ x < y | x = y.
26 [ #m #n #Hmn elim (nle_split_lt_eq … Hmn) -Hmn
27 /3 width=1 by or_introl, ylt_inj/
28 | #x @(ynat_split_nat_inf … x) -x
29 /2 width=1 by or_introl, ylt_inf/
34 lemma ynat_split_lt_ge (x) (y): ∨∨ x < y | y ≤ x.
35 #x #y elim (ynat_split_le_ge x y) /2 width=1 by or_intror/
36 #H elim (yle_split_lt_eq … H) -H /2 width=1 by or_introl, or_intror/
40 lemma ynat_split_lt_eq_gt (x) (y): ∨∨ x < y | y = x | y < x.
41 #x #y elim (ynat_split_lt_ge x y) /2 width=1 by or3_intro0/
42 #H elim (yle_split_lt_eq … H) -H /2 width=1 by or3_intro1, or3_intro2/
46 lemma ylt_yle_trans (x) (y) (z): y ≤ z → x < y → x < z.
48 [ #n #o #Hno #H elim (ylt_inv_inj_dx … H) -H
49 #m #Hmn #H destruct /3 width=3 by ylt_inj, nlt_nle_trans/
50 | #y /2 width=2 by ylt_des_lt_inf_dx/
55 lemma yle_ylt_trans (x) (y) (z): y < z → x ≤ y → x < z.
57 [ #n #o #Hno #H elim (yle_inv_inj_dx … H) -H
58 #m #Hmn #H destruct /3 width=3 by ylt_inj, nle_nlt_trans/
59 | #n #H elim (yle_inv_inj_dx … H) -H #m #_ #H destruct //
64 lemma nle_ylt_trans (m) (n) (z):
65 m ≤ n → yinj_nat n < z → yinj_nat m < z.
66 /3 width=3 by yle_ylt_trans, yle_inj/ qed-.
68 (* Inversions with yle ******************************************************)
71 lemma ylt_ge_false (x) (y): x < y → y ≤ x → ⊥.
72 /3 width=4 by yle_ylt_trans, ylt_inv_refl/ qed-.
74 (* Destructions with yle ****************************************************)
77 lemma ylt_des_le (x) (y): x < y → x ≤ y.
79 /3 width=1 by nlt_des_le, yle_inj/
82 (* Eliminations *************************************************************)
84 (*** ynat_ind_lt_le_aux *)
85 lemma ynat_ind_lt_le_inj_dx (Q:predicate …):
86 (∀y. (∀x. x < y → Q x) → Q y) →
87 ∀n,x. x ≤ yinj_nat n → Q x.
89 elim (yle_inv_inj_dx … H) -H #m #Hmn #H destruct
90 @(nat_ind_lt_le … Hmn) -Hmn #n0 #IH0
92 elim (ylt_inv_inj_dx … H) -H #m0 #Hmn0 #H destruct
96 (*** ynat_ind_lt_aux *)
97 lemma ynat_ind_lt_inj (Q:predicate …):
98 (∀y. (∀x. x < y → Q x) → Q y) →
100 /4 width=2 by ynat_ind_lt_le_inj_dx/ qed-.
103 lemma ynat_ind_lt (Q:predicate …):
104 (∀y. (∀x. x < y → Q x) → Q y) →
106 #Q #IH #y @(ynat_split_nat_inf … y) -y
107 [ /4 width=1 by ynat_ind_lt_inj/
109 elim (ylt_des_gen_sn … H) -H #m #H destruct
110 /4 width=1 by ynat_ind_lt_inj/