No title

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
Require Import Omega.

Theorem OmegaBasic:  forall (n m p : nat), n <= m ->  m <= p -> n <= p + 17.
Proof.

exact ((fun (n m p : nat) (H : n <= m) (H0 : m <= p) =>
 Decidable.dec_not_not (n <= p + 17) (dec_le n (p + 17))
   (fun H1 : ~ n <= p + 17 =>
    (fun H2 : n > p + 17 =>
     (fun H3 : (Z.of_nat n <= Z.of_nat m)%Z =>
      (fun H4 : (Z.of_nat m <= Z.of_nat p)%Z =>
       (fun (P : Z -> Prop) (H5 : P (Z.of_nat p + Z.of_nat 17)%Z) => eq_ind_r P H5 (Nat2Z.inj_add p 17))
         (fun x : Z => (Z.of_nat n > x)%Z -> False)
         (fun H5 : (Z.of_nat n > Z.of_nat p + 17)%Z =>
          ex_ind
            (fun (Zvar0 : Z) (Omega8 : Z.of_nat n = Zvar0 /\ (0 <= Zvar0 * 1 + 0)%Z) =>
             and_ind
               (fun (Omega0 : Z.of_nat n = Zvar0) (_ : (0 <= Zvar0 * 1 + 0)%Z) =>
                ex_ind
                  (fun (Zvar1 : Z) (Omega7 : Z.of_nat p = Zvar1 /\ (0 <= Zvar1 * 1 + 0)%Z) =>
                   and_ind
                     (fun (Omega1 : Z.of_nat p = Zvar1) (_ : (0 <= Zvar1 * 1 + 0)%Z) =>
                      ex_ind
                        (fun (Zvar2 : Z) (Omega6 : Z.of_nat m = Zvar2 /\ (0 <= Zvar2 * 1 + 0)%Z) =>
                         and_ind
                           (fun (Omega3 : Z.of_nat m = Zvar2) (_ : (0 <= Zvar2 * 1 + 0)%Z) =>
                            (fun (P : Z -> Prop) (H6 : P Zvar2) => eq_ind_r P H6 Omega3)
                              (fun x : Z => (0 <= x + - Z.of_nat n)%Z -> False)
                              ((fun (P : Z -> Prop) (H6 : P Zvar0) => eq_ind_r P H6 Omega0)
                                 (fun x : Z => (0 <= Zvar2 + - x)%Z -> False)
                                 (fast_Zopp_eq_mult_neg_1 Zvar0
                                    (fun x : Z => (0 <= Zvar2 + x)%Z -> False)
                                    (fast_Zred_factor0 Zvar2
                                       (fun x : Z => (0 <= x + Zvar0 * -1)%Z -> False)
                                       (fast_Zred_factor6 (Zvar0 * -1)
                                          (fun x : Z => (0 <= Zvar2 * 1 + x)%Z -> False)
                                          (fun Omega5 : (0 <= Zvar2 * 1 + (Zvar0 * -1 + 0))%Z =>
                                           (fun (P : Z -> Prop) (H6 : P Zvar1) => eq_ind_r P H6 Omega1)
                                             (fun x : Z => (0 <= x + - Z.of_nat m)%Z -> False)
                                             ((fun (P : Z -> Prop) (H6 : P Zvar2) =>
                                               eq_ind_r P H6 Omega3)
                                                (fun x : Z => (0 <= Zvar1 + - x)%Z -> False)
                                                (fast_Zopp_eq_mult_neg_1 Zvar2
                                                   (fun x : Z => (0 <= Zvar1 + x)%Z -> False)
                                                   (fast_Zplus_comm Zvar1 (Zvar2 * -1)
                                                      (fun x : Z => (0 <= x)%Z -> False)
                                                      (fast_Zred_factor0 Zvar1
                                                         (fun x : Z => (0 <= Zvar2 * -1 + x)%Z -> False)
                                                         (fast_Zred_factor6 
                                                            (Zvar1 * 1)
                                                            (fun x : Z =>
                                                             (0 <= Zvar2 * -1 + x)%Z -> False)
                                                            (fun
                                                               Omega4 : (0 <=
                                                                         Zvar2 * -1 + (Zvar1 * 1 + 0))%Z
                                                             =>
                                                             (fun (P : Z -> Prop) (H6 : P Zvar0) =>
                                                              eq_ind_r P H6 Omega0)
                                                               (fun x : Z =>
                                                                (0 <= x + -1 + - (Z.of_nat p + 17))%Z ->
                                                                False)
                                                               ((fun (P : Z -> Prop) (H6 : P Zvar1) =>
                                                                 eq_ind_r P H6 Omega1)
                                                                  (fun x : Z =>
                                                                   (0 <= Zvar0 + -1 + - (x + 17))%Z ->
                                                                   False)
                                                                  (fast_Zopp_plus_distr Zvar1 17
                                                                     (fun x : Z =>
                                                                      (0 <= Zvar0 + -1 + x)%Z -> False)
                                                                     (fast_Zopp_eq_mult_neg_1 Zvar1
                                                                        (fun x : Z =>
                                                                         (0 <=
                                                                          Zvar0 + -1 + (x + - (17)))%Z ->
                                                                         False)
                                                                        (fast_Zplus_permute
                                                                          (Zvar0 + -1) 
                                                                          (Zvar1 * -1) 
                                                                          (-17)
                                                                          (fun x : Z =>
                                                                          (0 <= x)%Z -> False)
                                                                          (fast_Zplus_assoc_reverse
                                                                          Zvar0 
                                                                          (-1) 
                                                                          (-17)
                                                                          (fun x : Z =>
                                                                          (0 <= Zvar1 * -1 + x)%Z ->
                                                                          False)
                                                                          (fast_Zred_factor0 Zvar0
                                                                          (fun x : Z =>
                                                                          (0 <= Zvar1 * -1 + (x + -18))%Z ->
                                                                          False)
                                                                          (fun
                                                                          Omega2 : 
                                                                          (0 <=
                                                                          Zvar1 * -1 +
                                                                          (Zvar0 * 1 + -18))%Z =>
                                                                          (fun H6 : (1 > 0)%Z =>
                                                                          (fun H7 : (1 > 0)%Z =>
                                                                          (fun
                                                                          auxiliary_2
                                                                          auxiliary_1 : 
                                                                          (1 > 0)%Z =>
                                                                          fast_OMEGA10 Zvar2 1 
                                                                          (-1) 
                                                                          (Zvar0 * -1 + 0)
                                                                          (Zvar1 * 1 + 0) 1 1
                                                                          (fun x : Z =>
                                                                          (0 <= x)%Z -> False)
                                                                          (fast_Zred_factor5 Zvar2
                                                                          ((Zvar0 * -1 + 0) * 1 +
                                                                          (Zvar1 * 1 + 0) * 1)
                                                                          (fun x : Z =>
                                                                          (0 <= x)%Z -> False)
                                                                          (fast_OMEGA12 Zvar1 1
                                                                          ((Zvar0 * -1 + 0) * 1) 0 1
                                                                          (fun x : Z =>
                                                                          (0 <= x)%Z -> False)
                                                                          (fast_OMEGA11 Zvar0 
                                                                          (-1) 0 
                                                                          (0 * 1) 1
                                                                          (fun x : Z =>
                                                                          (0 <= Zvar1 * (1 * 1) + x)%Z ->
                                                                          False)
                                                                          (fun
                                                                          Omega12 : 
                                                                          (0 <=
                                                                          Zvar1 * 1 + (Zvar0 * -1 + 0))%Z
                                                                          =>
                                                                          fast_OMEGA13 Zvar1
                                                                          (Zvar0 * -1 + 0)
                                                                          (Zvar0 * 1 + -18) 1
                                                                          (fun x : Z =>
                                                                          (0 <= x)%Z -> False)
                                                                          (fast_OMEGA14 Zvar0 0 
                                                                          (-18) 1
                                                                          (fun x : Z =>
                                                                          (0 <= x)%Z -> False)
                                                                          (fun H8 : Gt <> Gt =>
                                                                          False_ind False (H8 eq_refl)))
                                                                          (OMEGA2
                                                                          (Zvar1 * 1 + (Zvar0 * -1 + 0))
                                                                          (Zvar1 * -1 +
                                                                          (Zvar0 * 1 + -18)) Omega12
                                                                          Omega2)))))
                                                                          (OMEGA7
                                                                          (Zvar2 * 1 + (Zvar0 * -1 + 0))
                                                                          (Zvar2 * -1 + (Zvar1 * 1 + 0))
                                                                          1 1 auxiliary_1 auxiliary_2
                                                                          Omega5 Omega4)) H7) eq_refl
                                                                          H6) eq_refl)))))))
                                                               (Zgt_left (Z.of_nat n) 
                                                                  (Z.of_nat p + 17) H5)))))))
                                             (Zle_left (Z.of_nat m) (Z.of_nat p) H4))))))
                              (Zle_left (Z.of_nat n) (Z.of_nat m) H3)) Omega6) 
                        (intro_Z m)) Omega7) (intro_Z p)) Omega8) (intro_Z n)) 
         (inj_gt n (p + 17) H2)) (inj_le m p H0)) (inj_le n m H)) (not_le n (p + 17) H1)))).
Qed.