DEFINITION aplus_asort_simpl()
TYPE =
       ∀g:G
         .∀h:nat
           .∀k:nat
             .∀n:nat
               .eq
                 A
                 aplus g (ASort k n) h
                 ASort (minus k h) (next_plus g n (minus h k))
BODY =
        assume g: G
        assume h: nat
        assume k: nat
        assume n: nat
          (h1) 
             suppose H: lt k h
                (h1) 
                   by (aplus_assoc . . . .)
                   we proved 
                      eq
                        A
                        aplus g (aplus g (ASort k n) k) (minus h k)
                        aplus g (ASort k n) (plus k (minus h k))
                   we proceed by induction on the previous result to prove 
                      eq
                        A
                        aplus g (ASort k n) (plus k (minus h k))
                        ASort (minus k h) (next_plus g n (minus h k))
                      case refl_equal : ⇒
                         the thesis becomes 
                         eq
                           A
                           aplus g (aplus g (ASort k n) k) (minus h k)
                           ASort (minus k h) (next_plus g n (minus h k))
                            (h1) 
                               by (minus_n_n .)
                               we proved eq nat O (minus k k)
                               we proceed by induction on the previous result to prove 
                                  eq
                                    A
                                    aplus g (ASort (minus k k) n) (minus h k)
                                    ASort (minus k h) (next_plus g n (minus h k))
                                  case refl_equal : ⇒
                                     the thesis becomes 
                                     eq
                                       A
                                       aplus g (ASort O n) (minus h k)
                                       ASort (minus k h) (next_plus g n (minus h k))
                                        (h1) 
                                           by (aplus_asort_O_simpl . . .)

                                              eq
                                                A
                                                aplus g (ASort O n) (minus h k)
                                                ASort O (next_plus g n (minus h k))
                                        end of h1
                                        (h2) 
                                           consider H
                                           we proved lt k h
                                           that is equivalent to le (S k) h
                                           by (le_S . . previous)
                                           we proved le (S k) (S h)
                                           by (le_S_n . . previous)
                                           we proved le k h
                                           by (O_minus . . previous)
eq nat (minus k h) O
                                        end of h2
                                        by (eq_ind_r . . . h1 . h2)

                                           eq
                                             A
                                             aplus g (ASort O n) (minus h k)
                                             ASort (minus k h) (next_plus g n (minus h k))

                                  eq
                                    A
                                    aplus g (ASort (minus k k) n) (minus h k)
                                    ASort (minus k h) (next_plus g n (minus h k))
                            end of h1
                            (h2) 
                               by (le_n .)
                               we proved le k k
                               by (aplus_asort_le_simpl . . . . previous)
eq A (aplus g (ASort k n) k) (ASort (minus k k) n)
                            end of h2
                            by (eq_ind_r . . . h1 . h2)

                               eq
                                 A
                                 aplus g (aplus g (ASort k n) k) (minus h k)
                                 ASort (minus k h) (next_plus g n (minus h k))

                      eq
                        A
                        aplus g (ASort k n) (plus k (minus h k))
                        ASort (minus k h) (next_plus g n (minus h k))
                end of h1
                (h2) 
                   consider H
                   we proved lt k h
                   that is equivalent to le (S k) h
                   by (le_S . . previous)
                   we proved le (S k) (S h)
                   by (le_S_n . . previous)
                   we proved le k h
                   by (le_plus_minus . . previous)
eq nat h (plus k (minus h k))
                end of h2
                by (eq_ind_r . . . h1 . h2)
                we proved 
                   eq
                     A
                     aplus g (ASort k n) h
                     ASort (minus k h) (next_plus g n (minus h k))

                lt k h
                  →(eq
                       A
                       aplus g (ASort k n) h
                       ASort (minus k h) (next_plus g n (minus h k)))
          end of h1
          (h2) 
             suppose H: le h k
                (h1) 
                   (h1) 
                      by (refl_equal . .)
                      we proved 
                         eq
                           A
                           ASort (minus k h) (next_plus g n O)
                           ASort (minus k h) (next_plus g n O)

                         eq
                           A
                           ASort (minus k h) n
                           ASort (minus k h) (next_plus g n O)
                   end of h1
                   (h2) 
                      by (O_minus . . H)
eq nat (minus h k) O
                   end of h2
                   by (eq_ind_r . . . h1 . h2)

                      eq
                        A
                        ASort (minus k h) n
                        ASort (minus k h) (next_plus g n (minus h k))
                end of h1
                (h2) 
                   by (aplus_asort_le_simpl . . . . H)
eq A (aplus g (ASort k n) h) (ASort (minus k h) n)
                end of h2
                by (eq_ind_r . . . h1 . h2)
                we proved 
                   eq
                     A
                     aplus g (ASort k n) h
                     ASort (minus k h) (next_plus g n (minus h k))

                le h k
                  →(eq
                       A
                       aplus g (ASort k n) h
                       ASort (minus k h) (next_plus g n (minus h k)))
          end of h2
          by (lt_le_e . . . h1 h2)
          we proved 
             eq
               A
               aplus g (ASort k n) h
               ASort (minus k h) (next_plus g n (minus h k))
       we proved 
          ∀g:G
            .∀h:nat
              .∀k:nat
                .∀n:nat
                  .eq
                    A
                    aplus g (ASort k n) h
                    ASort (minus k h) (next_plus g n (minus h k))