ge_dec =
  fun n m : nat => le_dec m n
     : forall n m : nat, {n >= m} + {~ n >= m}

le_dec =
  fun n m : nat =>
  let s := le_gt_dec n m in
  match s with
  | left l => left l
  | right g => right (gt_not_le n m g)
  end
       : forall n m : nat, {n <= m} + {~ n <= m}


le_gt_dec =
  fun n m : nat => le_lt_dec n m
       : forall n m : nat, {n <= m} + {n > m}

le_lt_dec =
  fun n m : nat =>
  nat_rec (fun n0 : nat => forall m0 : nat, {n0 <= m0} + {m0 < n0})
    (fun m0 : nat => left (Nat.le_0_l m0))
    (fun (n0 : nat) (IHn : forall m0 : nat, {n0 <= m0} + {m0 < n0}) (m0 : nat)
     =>
     match m0 as n1 return ({S n0 <= n1} + {n1 < S n0}) with
     | 0 => right (gt_le_S 0 (S n0) (lt_le_S 0 (S n0) (Nat.lt_0_succ n0)))
     | S m1 =>
         sumbool_rec
           (fun _ : {n0 <= m1} + {m1 < n0} => {S n0 <= S m1} + {S m1 < S n0})
           (fun a : n0 <= m1 => left (gt_le_S n0 (S m1) (le_n_S n0 m1 a)))
           (fun b : m1 < n0 => right (gt_le_S (S m1) (S n0) (lt_n_S m1 n0 b)))
           (IHn m1)
     end) n m
       : forall n m : nat, {n <= m} + {m < n}

gt_not_le =
  fun n m : nat =>
  let H :=
    (fun n0 m0 : nat => match Nat.lt_nge n0 m0 with
                        | conj x _ => x
                        end)
    :
    forall n0 m0 : nat, n0 < m0 -> ~ m0 <= n0 in
  H m n
       : forall n m : nat, n > m -> ~ n <= m