Require Import Omega.

Theorem solve_it_for_me
  : forall n m q,
    n + m < q * 2 - m ->
    m < q.
intros.
omega.
Qed.

Print solve_it_for_me.
(*
solve_it_for_me =
fun (n m q : nat) (H : n + m < q * 2 - m) =>
Decidable.dec_not_not (m < q) (dec_lt m q)
  (fun H0 : ~ m < q =>
   (fun H1 : m >= q =>
    (fun (P : Z -> Prop) (H2 : P (Z.of_nat n + Z.of_nat m)%Z) =>
     eq_ind_r P H2 (Nat2Z.inj_add n m))
      (fun x : Z => (x < Z.of_nat (q * 2 - m))%Z -> False)
      (sumbool_ind
         (fun _ : {m <= q * 2} + {m > q * 2} =>
          (Z.of_nat n + Z.of_nat m < Z.of_nat (q * 2 - m))%Z -> False)
         (fun Omega0 : m <= q * 2 =>
          (fun (P : Z -> Prop) (H2 : P (Z.of_nat (q * 2) - Z.of_nat m)%Z) =>
           eq_ind_r P H2 (Nat2Z.inj_sub (q * 2) m Omega0))
            (fun x : Z => (Z.of_nat n + Z.of_nat m < x)%Z -> False)
            ((fun (P : Z -> Prop) (H2 : P (Z.of_nat q * Z.of_nat 2)%Z) =>
              eq_ind_r P H2 (Nat2Z.inj_mul q 2))
               (fun x : Z =>
                (Z.of_nat m <= x)%Z ->
                (Z.of_nat n + Z.of_nat m < Z.of_nat (q * 2) - Z.of_nat m)%Z ->
                False)
               (fun _ : (Z.of_nat m <= Z.of_nat q * 2)%Z =>
                (fun (P : Z -> Prop) (H2 : P (Z.of_nat q * Z.of_nat 2)%Z) =>
                 eq_ind_r P H2 (Nat2Z.inj_mul q 2))
                  (fun x : Z =>
                   (Z.of_nat n + Z.of_nat m < x - Z.of_nat m)%Z -> False)
                  (fun
                     H2 : (Z.of_nat n + Z.of_nat m <
                           Z.of_nat q * 2 - Z.of_nat m)%Z =>
                   (fun H3 : (Z.of_nat m >= Z.of_nat q)%Z =>
                    ex_ind
                      (fun (Zvar0 : Z)
                         (Omega9 : Z.of_nat m = Zvar0 /\
                                   (0 <= Zvar0 * 1 + 0)%Z) =>
                       and_ind
                         (fun (Omega2 : Z.of_nat m = Zvar0)
                            (_ : (0 <= Zvar0 * 1 + 0)%Z) =>
                          ex_ind
                            (fun (Zvar1 : Z)
                               (Omega8 : Z.of_nat q = Zvar1 /\
                                         (0 <= Zvar1 * 1 + 0)%Z) =>
                             and_ind
                               (fun (Omega3 : Z.of_nat q = Zvar1)
                                  (_ : (0 <= Zvar1 * 1 + 0)%Z) =>
                                ex_ind
                                  (fun (Zvar2 : Z)
                                     (Omega7 : Z.of_nat n = Zvar2 /\
                                               (0 <= Zvar2 * 1 + 0)%Z) =>
                                   and_ind
                                     (fun (Omega4 : Z.of_nat n = Zvar2)
                                        (Omega12 : (0 <= Zvar2 * 1 + 0)%Z) =>
                                      (fun (P : Z -> Prop) (H4 : P Zvar1) =>
                                       eq_ind_r P H4 Omega3)
                                        (fun x : Z =>
                                         (0 <=
                                          x * 2 + - Z.of_nat m + -1 +
                                          - (Z.of_nat n + Z.of_nat m))%Z ->
                                         False)
                                        ((fun (P : Z -> Prop) (H4 : P Zvar0)
                                          => eq_ind_r P H4 Omega2)
                                           (fun x : Z =>
                                            (0 <=
                                             Zvar1 * 2 + - x + -1 +
                                             - (Z.of_nat n + Z.of_nat m))%Z ->
                                            False)
                                           (fast_Zopp_eq_mult_neg_1 Zvar0
                                              (fun x : Z =>
                                               (0 <=
                                                Zvar1 * 2 + x + -1 +
                                                - (Z.of_nat n + Z.of_nat m))%Z ->
                                               False)
                                              (fast_Zplus_comm (Zvar1 * 2)
                                                 (Zvar0 * -1)
                                                 (fun x : Z =>
                                                  (0 <=
                                                   x + -1 +
                                                   -
                                                   (Z.of_nat n + Z.of_nat m))%Z ->
                                                  False)
                                                 (fast_Zplus_assoc_reverse
                                                    (Zvar0 * -1) (Zvar1 * 2)
                                                    (-1)
                                                    (fun x : Z =>
                                                     (0 <=
                                                      x +
                                                      -
                                                      (Z.of_nat n +
                                                       Z.of_nat m))%Z ->
                                                     False)
                                                    ((fun (P : Z -> Prop)
                                                        (H4 : P Zvar2) =>
                                                      eq_ind_r P H4 Omega4)
                                                       (fun x : Z =>
                                                        (0 <=
                                                         Zvar0 * -1 +
                                                         (Zvar1 * 2 + -1) +
                                                         - (x + Z.of_nat m))%Z ->
                                                        False)
                                                       ((fun (P : Z -> Prop)
                                                           (H4 : P Zvar0) =>
                                                         eq_ind_r P H4 Omega2)
                                                          (fun x : Z =>
                                                           (0 <=
                                                            Zvar0 * -1 +
                                                            (Zvar1 * 2 + -1) +
                                                            - (Zvar2 + x))%Z ->
                                                           False)
                                                          (fast_Zopp_plus_distr
                                                             Zvar2 Zvar0
                                                             (fun x : Z =>
                                                              (0 <=
                                                               Zvar0 * -1 +
                                                               (Zvar1 * 2 +
                                                                -1) + x)%Z ->
                                                              False)
                                                             (fast_Zopp_eq_mult_neg_1
                                                                Zvar2
                                                                (fun x : Z =>
                                                                 (0 <=
                                                                  Zvar0 * -1 +
                                                                  (Zvar1 * 2 +
                                                                   -1) +
                                                                  (x +
                                                                   - Zvar0))%Z ->
                                                                 False)
                                                                (fast_Zopp_eq_mult_neg_1
                                                                   Zvar0
                                                                   (fun x : Z
                                                                    =>
                                                                    (0 <=
                                                                    Zvar0 *
                                                                    -1 +
                                                                    (Zvar1 *
                                                                    2 + -1) +
                                                                    (Zvar2 *
                                                                    -1 + x))%Z ->
                                                                    False)
                                                                   (fast_Zplus_permute
                                                                    (Zvar0 *
                                                                    -1 +
                                                                    (Zvar1 *
                                                                    2 + -1))
                                                                    (Zvar2 *
                                                                    -1)
                                                                    (Zvar0 *
                                                                    -1)
                                                                    (fun
                                                                    x : Z =>
                                                                    (0 <= x)%Z ->
                                                                    False)
                                                                    (fast_Zplus_comm
                                                                    (Zvar0 *
                                                                    -1 +
                                                                    (Zvar1 *
                                                                    2 + -1))
                                                                    (Zvar0 *
                                                                    -1)
                                                                    (fun
                                                                    x : Z =>
                                                                    (0 <=
                                                                    Zvar2 *
                                                                    -1 + x)%Z ->
                                                                    False)
                                                                    (fast_Zplus_assoc
                                                                    (Zvar0 *
                                                                    -1)
                                                                    (Zvar0 *
                                                                    -1)
                                                                    (Zvar1 *
                                                                    2 + -1)
                                                                    (fun
                                                                    x : Z =>
                                                                    (0 <=
                                                                    Zvar2 *
                                                                    -1 + x)%Z ->
                                                                    False)
                                                                    (fast_Zred_factor4
                                                                    Zvar0
                                                                    (-1)
                                                                    (-1)
                                                                    (fun
                                                                    x : Z =>
                                                                    (0 <=
                                                                    Zvar2 *
                                                                    -1 +
                                                                    (x +
                                                                    (Zvar1 *
                                                                    2 + -1)))%Z ->
                                                                    False)
                                                                    (fun
                                                                    Omega5 :
                                                                    (0 <=
                                                                    Zvar2 *
                                                                    -1 +
                                                                    (Zvar0 *
                                                                    -2 +
                                                                    (Zvar1 *
                                                                    2 + -1)))%Z
                                                                    =>
                                                                    (fun
                                                                    (P :
                                                                    Z -> Prop)
                                                                    (H4 :
                                                                    P Zvar0)
                                                                    =>
                                                                    eq_ind_r
                                                                    P H4
                                                                    Omega2)
                                                                    (fun
                                                                    x : Z =>
                                                                    (0 <=
                                                                    x +
                                                                    -
                                                                    Z.of_nat
                                                                    q)%Z ->
                                                                    False)
                                                                    ((fun
                                                                    (P :
                                                                    Z -> Prop)
                                                                    (H4 :
                                                                    P Zvar1)
                                                                    =>
                                                                    eq_ind_r
                                                                    P H4
                                                                    Omega3)
                                                                    (fun
                                                                    x : Z =>
                                                                    (0 <=
                                                                    Zvar0 +
                                                                    - x)%Z ->
                                                                    False)
                                                                    (fast_Zopp_eq_mult_neg_1
                                                                    Zvar1
                                                                    (fun
                                                                    x : Z =>
                                                                    (0 <=
                                                                    Zvar0 + x)%Z ->
                                                                    False)
                                                                    (fast_Zred_factor0
                                                                    Zvar0
                                                                    (fun
                                                                    x : Z =>
                                                                    (0 <=
                                                                    x +
                                                                    Zvar1 *
                                                                    -1)%Z ->
                                                                    False)
                                                                    (fast_Zred_factor6
                                                                    (Zvar1 *
                                                                    -1)
                                                                    (fun
                                                                    x : Z =>
                                                                    (0 <=
                                                                    Zvar0 * 1 +
                                                                    x)%Z ->
                                                                    False)
                                                                    (fun
                                                                    Omega6 :
                                                                    (0 <=
                                                                    Zvar0 * 1 +
                                                                    (Zvar1 *
                                                                    -1 + 0))%Z
                                                                    =>
                                                                    let H4 :=
                                                                    eq_refl
                                                                    :
                                                                    (1 > 0)%Z
                                                                    in
                                                                    (let
                                                                    H5 :=
                                                                    eq_refl
                                                                    :
                                                                    (1 > 0)%Z
                                                                    in
                                                                    (fun
                                                                    auxiliary_2
                                                                    auxiliary_1 :
                                                                    (1 > 0)%Z
                                                                    =>
                                                                    fast_OMEGA10
                                                                    Zvar2 1
                                                                    (-1) 0
                                                                    (Zvar0 *
                                                                    -2 +
                                                                    (Zvar1 *
                                                                    2 + -1))
                                                                    1 1
                                                                    (fun
                                                                    x : Z =>
                                                                    (0 <= x)%Z ->
                                                                    False)
                                                                    (fast_Zred_factor5
                                                                    Zvar2
                                                                    (0 +
                                                                    (Zvar0 *
                                                                    -2 +
                                                                    (Zvar1 *
                                                                    2 + -1)) *
                                                                    1)
                                                                    (fun
                                                                    x : Z =>
                                                                    (0 <= x)%Z ->
                                                                    False)
                                                                    (fast_OMEGA12
                                                                    Zvar0
                                                                    (-2) 0
                                                                    (Zvar1 *
                                                                    2 + -1) 1
                                                                    (fun
                                                                    x : Z =>
                                                                    (0 <= x)%Z ->
                                                                    False)
                                                                    (fast_OMEGA12
                                                                    Zvar1 2 0
                                                                    (-1) 1
                                                                    (fun
                                                                    x : Z =>
                                                                    (0 <=
                                                                    Zvar0 *
                                                                    (-2 * 1) +
                                                                    x)%Z ->
                                                                    False)
                                                                    (fun
                                                                    Omega13 :
                                                                    (0 <=
                                                                    Zvar0 *
                                                                    -2 +
                                                                    (Zvar1 *
                                                                    2 + -1))%Z
                                                                    =>
                                                                    let H6 :=
                                                                    fast_OMEGA11
                                                                    Zvar0
                                                                    (-1)
                                                                    (Zvar1 *
                                                                    1 + -1) 1
                                                                    2
                                                                    (fun
                                                                    x : Z =>
                                                                    (Zvar0 *
                                                                    -2 +
                                                                    (Zvar1 *
                                                                    2 + -1))%Z =
                                                                    x)
                                                                    (fast_OMEGA11
                                                                    Zvar1 1
                                                                    (-1) 1 2
                                                                    (fun
                                                                    x : Z =>
                                                                    (Zvar0 *
                                                                    -2 +
                                                                    (Zvar1 *
                                                                    2 + -1))%Z =
                                                                    (Zvar0 *
                                                                    (-1 * 2) +
                                                                    x)%Z)
                                                                    eq_refl)
                                                                    :
                                                                    (Zvar0 *
                                                                    -2 +
                                                                    (Zvar1 *
                                                                    2 + -1))%Z =
                                                                    ((Zvar0 *
                                                                    -1 +
                                                                    (Zvar1 *
                                                                    1 + -1)) *
                                                                    2 + 1)%Z
                                                                    in
                                                                    (fun
                                                                    auxiliary :
                                                                    (Zvar0 *
                                                                    -2 +
                                                                    (Zvar1 *
                                                                    2 + -1))%Z =
                                                                    ((Zvar0 *
                                                                    -1 +
                                                                    (Zvar1 *
                                                                    1 + -1)) *
                                                                    2 + 1)%Z
                                                                    =>
                                                                    (fun
                                                                    Omega14 :
                                                                    (0 <=
                                                                    (Zvar0 *
                                                                    -1 +
                                                                    (Zvar1 *
                                                                    1 + -1)) *
                                                                    2 + 1)%Z
                                                                    =>
                                                                    let H7 :=
                                                                    eq_refl
                                                                    :
                                                                    (2 > 1)%Z
                                                                    in
                                                                    (let
                                                                    H8 :=
                                                                    eq_refl
                                                                    :
                                                                    (2 > 0)%Z
                                                                    in
                                                                    (fun
                                                                    (auxiliary_3 :
                                                                    (2 > 0)%Z)
                                                                    (auxiliary_4 :
                                                                    (2 > 1)%Z)
                                                                    =>
                                                                    (fun
                                                                    Omega15 :
                                                                    (0 <=
                                                                    Zvar0 *
                                                                    -1 +
                                                                    (Zvar1 *
                                                                    1 + -1))%Z
                                                                    =>
                                                                    fast_OMEGA13
                                                                    Zvar0
                                                                    (Zvar1 *
                                                                    -1 + 0)
                                                                    (Zvar1 *
                                                                    1 + -1) 1
                                                                    (fun
                                                                    x : Z =>
                                                                    (0 <= x)%Z ->
                                                                    False)
                                                                    (fast_OMEGA14
                                                                    Zvar1 0
                                                                    (-1) 1
                                                                    (fun
                                                                    x : Z =>
                                                                    (0 <= x)%Z ->
                                                                    False)
                                                                    (fun
                                                                    H9 :
                                                                    Gt <> Gt
                                                                    =>
                                                                    False_ind
                                                                    False
                                                                    (H9
                                                                    eq_refl)))
                                                                    (OMEGA2
                                                                    (Zvar0 *
                                                                    1 +
                                                                    (Zvar1 *
                                                                    -1 + 0))
                                                                    (Zvar0 *
                                                                    -1 +
                                                                    (Zvar1 *
                                                                    1 + -1))
                                                                    Omega6
                                                                    Omega15))
                                                                    (Zmult_le_approx
                                                                    2
                                                                    (Zvar0 *
                                                                    -1 +
                                                                    (Zvar1 *
                                                                    1 + -1))
                                                                    1
                                                                    auxiliary_3
                                                                    auxiliary_4
                                                                    Omega14))
                                                                    H8) H7)
                                                                    (OMEGA1
                                                                    (Zvar0 *
                                                                    -2 +
                                                                    (Zvar1 *
                                                                    2 + -1))
                                                                    ((Zvar0 *
                                                                    -1 +
                                                                    (Zvar1 *
                                                                    1 + -1)) *
                                                                    2 + 1)
                                                                    auxiliary
                                                                    Omega13))
                                                                    H6))))
                                                                    (OMEGA7
                                                                    (Zvar2 *
                                                                    1 + 0)
                                                                    (Zvar2 *
                                                                    -1 +
                                                                    (Zvar0 *
                                                                    -2 +
                                                                    (Zvar1 *
                                                                    2 + -1)))
                                                                    1 1
                                                                    auxiliary_1
                                                                    auxiliary_2
                                                                    Omega12
                                                                    Omega5))
                                                                    H5) H4)))))
                                                                    (Zge_left
                                                                    (Z.of_nat
                                                                    m)
                                                                    (Z.of_nat
                                                                    q) H3)))))))))))))))
                                        (Zlt_left (Z.of_nat n + Z.of_nat m)
                                           (Z.of_nat q * 2 - Z.of_nat m) H2))
                                     Omega7) (intro_Z n)) Omega8) (intro_Z q))
                         Omega9) (intro_Z m)) (inj_ge m q H1)))
               (inj_le m (q * 2) Omega0)))
         (fun Omega0 : m > q * 2 =>
          (fun (P : Z -> Prop) (H2 : P 0%Z) =>
           eq_ind_r P H2 (inj_minus2 (q * 2) m Omega0))
            (fun x : Z => (Z.of_nat n + Z.of_nat m < x)%Z -> False)
            ((fun (P : Z -> Prop) (H2 : P (Z.of_nat q * Z.of_nat 2)%Z) =>
              eq_ind_r P H2 (Nat2Z.inj_mul q 2))
               (fun x : Z =>
                (Z.of_nat m > x)%Z ->
                (Z.of_nat n + Z.of_nat m < 0)%Z -> False)
               (fun (_ : (Z.of_nat m > Z.of_nat q * 2)%Z)
                  (H2 : (Z.of_nat n + Z.of_nat m < 0)%Z) =>
                (fun _ : (Z.of_nat m >= Z.of_nat q)%Z =>
                 ex_ind
                   (fun (Zvar3 : Z)
                      (Omega20 : Z.of_nat m = Zvar3 /\ (0 <= Zvar3 * 1 + 0)%Z)
                    =>
                    and_ind
                      (fun (Omega12 : Z.of_nat m = Zvar3)
                         (Omega21 : (0 <= Zvar3 * 1 + 0)%Z) =>
                       ex_ind
                         (fun (Zvar4 : Z)
                            (Omega19 : Z.of_nat q = Zvar4 /\
                                       (0 <= Zvar4 * 1 + 0)%Z) =>
                          and_ind
                            (fun (_ : Z.of_nat q = Zvar4)
                               (_ : (0 <= Zvar4 * 1 + 0)%Z) =>
                             ex_ind
                               (fun (Zvar5 : Z)
                                  (Omega18 : Z.of_nat n = Zvar5 /\
                                             (0 <= Zvar5 * 1 + 0)%Z) =>
                                and_ind
                                  (fun (Omega15 : Z.of_nat n = Zvar5)
                                     (Omega23 : (0 <= Zvar5 * 1 + 0)%Z) =>
                                   (fun (P : Z -> Prop) (H4 : P Zvar5) =>
                                    eq_ind_r P H4 Omega15)
                                     (fun x : Z =>
                                      (0 <= -1 + - (x + Z.of_nat m))%Z ->
                                      False)
                                     ((fun (P : Z -> Prop) (H4 : P Zvar3) =>
                                       eq_ind_r P H4 Omega12)
                                        (fun x : Z =>
                                         (0 <= -1 + - (Zvar5 + x))%Z -> False)
                                        (fast_Zopp_plus_distr Zvar5 Zvar3
                                           (fun x : Z =>
                                            (0 <= -1 + x)%Z -> False)
                                           (fast_Zopp_eq_mult_neg_1 Zvar5
                                              (fun x : Z =>
                                               (0 <= -1 + (x + - Zvar3))%Z ->
                                               False)
                                              (fast_Zopp_eq_mult_neg_1 Zvar3
                                                 (fun x : Z =>
                                                  (0 <= -1 + (Zvar5 * -1 + x))%Z ->
                                                  False)
                                                 (fast_Zplus_permute
                                                    (-1) (Zvar5 * -1)
                                                    (Zvar3 * -1)
                                                    (fun x : Z =>
                                                     (0 <= x)%Z -> False)
                                                    (fast_Zplus_comm
                                                       (-1) (Zvar3 * -1)
                                                       (fun x : Z =>
                                                        (0 <= Zvar5 * -1 + x)%Z ->
                                                        False)
                                                       (fun
                                                          Omega16 : (0 <=
                                                                    Zvar5 *
                                                                    -1 +
                                                                    (Zvar3 *
                                                                    -1 + -1))%Z
                                                        =>
                                                        let H4 :=
                                                          eq_refl : (1 > 0)%Z
                                                          in
                                                        (let H5 :=
                                                           eq_refl
                                                           :
                                                           (1 > 0)%Z in
                                                         (fun
                                                            auxiliary_2
                                                             auxiliary_1 :
                                                             (1 > 0)%Z =>
                                                          fast_OMEGA12 Zvar5
                                                            (-1)
                                                            ((Zvar3 * 1 + 0) *
                                                             1)
                                                            (Zvar3 * -1 + -1)
                                                            1
                                                            (fun x : Z =>
                                                             (0 <= x)%Z ->
                                                             False)
                                                            (fast_OMEGA10
                                                               Zvar3 1
                                                               (-1) 0
                                                               (-1) 1 1
                                                               (fun x : Z =>
                                                                (0 <=
                                                                 Zvar5 *
                                                                 (-1 * 1) + x)%Z ->
                                                                False)
                                                               (fast_Zred_factor5
                                                                  Zvar3
                                                                  (0 + -1 * 1)
                                                                  (fun x : Z
                                                                   =>
                                                                   (0 <=
                                                                    Zvar5 *
                                                                    (-1 * 1) +
                                                                    x)%Z ->
                                                                   False)
                                                                  (fun
                                                                    Omega24 :
                                                                    (0 <=
                                                                    Zvar5 *
                                                                    -1 + -1)%Z
                                                                   =>
                                                                   fast_OMEGA13
                                                                    Zvar5 0
                                                                    (-1) 1
                                                                    (fun
                                                                    x : Z =>
                                                                    (0 <= x)%Z ->
                                                                    False)
                                                                    (fun
                                                                    H6 :
                                                                    Gt <> Gt
                                                                    =>
                                                                    False_ind
                                                                    False
                                                                    (H6
                                                                    eq_refl))
                                                                    (OMEGA2
                                                                    (Zvar5 *
                                                                    1 + 0)
                                                                    (Zvar5 *
                                                                    -1 + -1)
                                                                    Omega23
                                                                    Omega24))))
                                                            (OMEGA7
                                                               (Zvar3 * 1 + 0)
                                                               (Zvar5 * -1 +
                                                                (Zvar3 * -1 +
                                                                 -1)) 1 1
                                                               auxiliary_1
                                                               auxiliary_2
                                                               Omega21
                                                               Omega16)) H5)
                                                          H4)))))))
                                     (Zlt_left (Z.of_nat n + Z.of_nat m) 0 H2))
                                  Omega18) (intro_Z n)) Omega19) (intro_Z q))
                      Omega20) (intro_Z m)) (inj_ge m q H1))
               (inj_gt m (q * 2) Omega0))) (le_gt_dec m (q * 2)))
      (inj_lt (n + m) (q * 2 - m) H)) (not_lt m q H0))
     : forall n m q : nat, n + m < q * 2 - m -> m < q

Argument scopes are [nat_scope nat_scope nat_scope _]

*)