omega

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
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 + .)%Z -> False)
                                      (fast_Zred_factor6 (Zvar0 * -1)
                                         (fun x : Z => (.)%Z -> False)
                                         (fun Omega5 : .%Z => (.) (.) (.) (.))))))
                             (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))