module ProofColDivSeqPostulate

import ProofColDivSeqBase

%default total
-- %language ElabReflection
%access export

%hide Language.Reflection.P

--            from ProofColDivSeqBase
-- ########################################
public export
data Limited : CoList Integer -> Type where
  IsLimited00 : (step : Nat ** limitedNStep xs step = True) -> Limited xs
  IsLimited01 : (k : Nat)
    -> Limited $ divSeq (plus (plus k k) k)
      -> Limited $ divSeq (S (plus (plus (plus (plus (plus k k) (plus k k)) (plus k k))
                                         (S (plus (plus (plus k k) (plus k k))(plus k k))))
                                   (S (plus (plus (plus k k) (plus k k)) (plus k k)))))
  IsLimited02 : (l : Nat)
    -> Limited (divSeq (plus (plus (plus l l) (plus l l)) (plus l l))) 
      -> Limited (divSeq (S (S (plus (plus (plus (plus (plus (plus (plus l l) l) (plus (plus l l) l))
                                                       (S (plus (plus (plus l l) l) (plus (plus l l) l))))
                                                 (S (plus (plus (plus l l) l) (plus (plus l l) l))))
                                           (S (S (plus (plus (plus (plus (plus l l) l) (plus (plus l l) l))
                                                             (S (plus (plus (plus l l) l) (plus (plus l l) l))))
                                                       (S (plus (plus (plus l l) l) (plus (plus l l) l)))))))
                                     (S (S (plus (plus (plus (plus (plus l l) l) (plus (plus l l) l))
                                                       (S (plus (plus (plus l l) l) (plus (plus l l) l))))
                                                 (S (plus (plus (plus l l) l) (plus (plus l l) l))))))))))
  IsLimited03 : (l : Nat)
    -> Limited (divSeq (S (S (S (plus (plus (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l)))
                                            (S (S (S (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l)))))))
                                      (S (S (S (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l)))))))))))
     -> Limited (divSeq (S (S (S (plus (plus (plus (plus (plus (plus (plus l l) l) (S (plus (plus l l) l)))
                                                         (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))
                                                   (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))
                                             (S (S (S (plus (plus (plus (plus (plus l l) l) (S (plus (plus l l) l)))
                                                                  (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))
                                                            (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))))))
                                       (S (S (S (plus (plus (plus (plus (plus l l) l) (S (plus (plus l l) l)))
                                                            (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))
                                                      (S (S (plus (plus (plus l l) l) (S (plus (plus l l) l))))))))))))))
  IsLimited04 : (l : Nat)
    -> Limited (divSeq (S (S (S (plus (plus (plus (plus l l) (plus l l))
                                            (S (S (S (plus (plus l l) (plus l l))))))
                                      (S (S (S (plus (plus l l) (plus l l))))))))))
      -> Limited (divSeq (S (S (S (S (plus (plus (plus (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                                                             (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                                       (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                                 (S (S (S (S (plus (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                                                                         (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                                                   (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l)))))))))))))
                                           (S (S (S (S (plus (plus (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))
                                                                   (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))
                                                             (S (S (S (plus (plus (plus l l) l) (S (S (plus (plus l l) l))))))))))))))))))
  IsLimited05 : (j : Nat)
    -> Limited (divSeq (plus (plus j j) j))
      -> Limited (divSeq (S (S (plus (plus (plus (plus j j) j) (S (S (plus (plus j j) j))))
                                     (S (S (plus (plus j j) j)))))))
  IsLimited06 : (l : Nat)
    -> Limited (divSeq (plus (plus l l) l))
      -> Limited (divSeq (S (S (S (plus (plus (plus (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l))) (plus (plus l l) (plus l l)))
                                              (S (S (S (plus (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l))) (plus (plus l l) (plus l l)))))))
                                        (S (S (S (plus (plus (plus (plus l l) (plus l l)) (plus (plus l l) (plus l l))) (plus (plus l l) (plus l l)))))))))))
  IsLimited07 : (o : Nat)
    -> Limited (divSeq (S (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus (plus o o)
                                                                               (plus o o))
                                                                         (plus (plus o o) (plus o o)))
                                                                   (plus (plus (plus o o) (plus o o))
                                                                         (plus (plus o o) (plus o o))))
                                                             (plus (plus (plus (plus o o) (plus o o))
                                                                         (plus (plus o o) (plus o o)))
                                                                   (plus (plus (plus o o) (plus o o))
                                                                         (plus (plus o o) (plus o o)))))
                                                       (S (S (S (S (S (S (S (plus (plus (plus (plus (plus o o)
                                                                                                    (plus o o))   
                                                                                              (plus (plus o o)    
                                                                                                    (plus o o)))
                                                                                        (plus (plus (plus o o)    
                                                                                                    (plus o o))   
                                                                                              (plus (plus o o)    
                                                                                                    (plus o o)))) 
                                                                                  (plus (plus (plus (plus o o)
                                                                                                    (plus o o))   
                                                                                              (plus (plus o o)    
                                                                                                    (plus o o)))  
                                                                                        (plus (plus (plus o o)
                                                                                                    (plus o o))   
                                                                                              (plus (plus o o)    
                                                                                                    (plus o       
                                                                                                          o)))))))))))))
                                                 (S (S (S (S (S (S (S (plus (plus (plus (plus (plus o o)
                                                                                              (plus o o))
                                                                                        (plus (plus o o)
                                                                                              (plus o o)))
                                                                                  (plus (plus (plus o o)
                                                                                              (plus o o))
                                                                                        (plus (plus o o)
                                                                                              (plus o o))))
                                                                            (plus (plus (plus (plus o o)
                                                                                              (plus o o))
                                                                                        (plus (plus o o)
                                                                                              (plus o o)))
                                                                                  (plus (plus (plus o o)
                                                                                              (plus o o))
                                                                                        (plus (plus o o)
                                                                                              (plus o
                                                                                                    o)))))))))))))))))))))
      -> Limited (divSeq (S (S (S (S (plus (plus (plus (plus (plus (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))
                                                                 (S (plus (plus (plus o o) o)
                                                                          (plus (plus o o) o))))
                                                           (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o)
                                                                             (plus (plus o o) o))))))
                                                     (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                              (S (plus (plus (plus o o) o)
                                                                       (plus (plus o o) o))))))
                                               (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o)
                                                                                   (plus (plus o o) o))
                                                                             (S (plus (plus (plus o o) o)
                                                                                      (plus (plus o o) o))))
                                                                       (S (plus (plus (plus (plus o o) o)
                                                                                      (plus (plus o o) o))
                                                                                (S (plus (plus (plus o o) o)
                                                                                         (plus (plus o o) o))))))
                                                                 (S (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                          (S (plus (plus (plus o o) o)
                                                                                   (plus (plus o o) o)))))))))))
                                         (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o)
                                                                             (plus (plus o o) o))
                                                                       (S (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))))
                                                                 (S (plus (plus (plus (plus o o) o)
                                                                                (plus (plus o o) o))
                                                                          (S (plus (plus (plus o o) o)
                                                                                   (plus (plus o o) o))))))
                                                           (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o)
                                                                             (plus (plus o o) o))))))))))))))))
  IsLimited08 : (o : Nat)
    -> Limited (divSeq (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) (plus o o))
                                                                         (plus (plus o o) (plus o o)))
                                                                   (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                                             (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o))
                                                                                                    (plus (plus o o) (plus o o)))
                                                                                              (plus (plus (plus o o) (plus o o))
                                                                                                    (plus (plus o o) (plus o o)))))))))))))) (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o))
                                                                                              (plus (plus o o) (plus o o)))
                                                                                        (plus (plus (plus o o) (plus o o))
                                                                                              (plus (plus o o)
                                                                                                    (plus o o))))))))))))))))))))))))
      -> Limited (divSeq (S (S (S (S (S (plus (plus (plus (plus (plus (plus (plus (plus o o) o)
                                                                          (S (plus (plus o o) o)))
                                                                    (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                                              (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                                        (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                    (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))
                                                  (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                   (S (S (plus (plus (plus o o) o)
                                                                                               (S (plus (plus o o) o))))))
                                                                             (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                         (S (S (plus (plus (plus o o) o)
                                                                                                     (S (plus (plus o o) o)))))))))
                                                                       (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                   (S (S (plus (plus (plus o o) o)
                                                                                               (S (plus (plus o o) o)))))))))))))))
                                            (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                             (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                                                       (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                   (S (S (plus (plus (plus o o) o)
                                                                                               (S (plus (plus o o) o)))))))))
                                                                 (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                             (S (S (plus (plus (plus o o) o)
                                                                                         (S (plus (plus o o) o)))))))))))))))))))))
  IsLimited09 : (o : Nat)
    -> Limited $ divSeq (S (S (S (S (S (S (S (plus (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))
                                                         (S (S (S (S (S (S (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))))))))
                                                   (S (S (S (S (S (S (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))))))))))))))
      -> Limited $ divSeq (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                       (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))
                                                                 (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))
                                                           (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                          (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))
                                                     (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                         (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))
                                                                                   (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                                  (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))
                                                                             (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                            (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))))))))))
                                               (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                   (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))
                                                                             (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                            (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))
                                                                       (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                      (S (S (S (plus (plus (plus o o) o)
                                                                                                     (S (S (plus (plus o o) o)))))))))))))))))))))))))
  IsLimited10 : (o : Nat)
    -> Limited $ divSeq (S (plus (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))
                                       (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))
                                 (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))
      -> Limited $ divSeq (S (S (S (S (plus (plus (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                 (plus (plus (plus o o) o) (plus (plus o o) o)))
                                                           (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))))
                                                     (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))))
                                               (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o))) (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                (plus (plus (plus o o) o) (plus (plus o o) o)))))
                                                                 (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                          (plus (plus (plus o o) o) (plus (plus o o) o))))))))))
                                         (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))
                                                                 (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (plus (plus (plus o o) o) (plus (plus o o) o)))))
                                                           (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                    (plus (plus (plus o o) o) (plus (plus o o) o))))))))))))))
  IsLimited11 : (o : Nat)
    -> Limited $ divSeq (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus (plus o o) (plus o o))
                                                                                                 (plus (plus o o) (plus o o)))
                                                                                           (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                                                                     (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))
                                                                                           (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))
                                                                               (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus (plus o o) (plus o o))
                                                                                                                                              (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o))
                                                                                                                                              (plus (plus o o)
                                                                                                                                                    (plus o o))))
                                                                                                                                  (plus (plus (plus (plus o o) (plus o o))
                                                                                                                                              (plus (plus o o) (plus o o))) (plus (plus (plus o o) (plus o o))
                                                                                                                                              (plus (plus o o)
                                                                                                                                                    (plus o o)))))))))))))))))))))
                                                                         (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus (plus o o) (plus o o))
                                                                                                                                        (plus (plus o o) (plus o o)))
                                                                                                                                  (plus (plus (plus o o) (plus o o))
                                                                                                                                        (plus (plus o o) (plus o o))))
                                                                                                                            (plus (plus (plus (plus o o) (plus o o))
                                                                                                                                        (plus (plus o o) (plus o o)))
                                                                                                                                  (plus (plus (plus o o) (plus o o))
                                                                                                                                        (plus (plus o o)
                                                                                                                                              (plus o o))))))))))))))))))))))))))))))))))))
      -> Limited $ divSeq (S (S (S (S (S (plus (plus (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                    (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))
                                                              (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                          (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                                                        (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                    (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                                                  (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                   (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))
                                                                             (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                         (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                                                                       (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                   (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))))))
                                            (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                             (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))
                                                                       (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                   (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))
                                                                 (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                             (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))))))))))))
  IsLimited12 : (o : Nat)
    -> Limited $ divSeq (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))
                                                                               (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                                                         (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o))
                                                                                                                            (plus (plus o o) (plus o o)))
                                                                                                                      (plus (plus (plus o o) (plus o o))
                                                                                                                            (plus (plus o o) (plus o o))))))))))))))))))
                                                                   (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o))
                                                                                                                      (plus (plus o o) (plus o o)))
                                                                                                                (plus (plus (plus o o) (plus o o))
                                                                                                                      (plus (plus o o)
                                                                                                                            (plus o o)))))))))))))))))))))))))))))))
      -> Limited $ divSeq (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                       (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                                                 (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))
                                                           (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                          (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))
                                                     (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                         (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                                                                   (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                                  (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))
                                                                             (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                            (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))))))))
                                               (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                   (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))
                                                                             (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                            (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))
                                                                       (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                      (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))))))))))))))))))
  IsLimited13 : (o : Nat)
    -> Limited $ divSeq (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))
                                                       (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))
                                                 (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))
                                                                      (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))))))
                                           (S (S (S (S (S (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))
                                                                (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))))))))))))
      -> Limited $ divSeq (S (S (S (S (S (plus (plus (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                    (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                              (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                          (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
                                                        (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o)) (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
                                                  (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                   (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                             (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                         (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
                                                                       (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                   (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))))))))
                                            (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                             (S (plus (plus (plus o o) o) (plus (plus o o) o))))
                                                                       (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                                   (S (plus (plus (plus o o) o) (plus (plus o o) o)))))))
                                                                 (S (S (plus (plus (plus (plus o o) o) (plus (plus o o) o))
                                                                             (S (plus (plus (plus o o) o) (plus (plus o o) o))))))))))))))))))
  IsLimited14 : (o : Nat)
    -> Limited $ divSeq (S (S (S (S (S (plus (plus (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))
                                                 (S (S (S (S (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o)))))))))
                                           (S (S (S (S (S (plus (plus (plus o o) (plus o o)) (plus (plus o o) (plus o o))))))))))))))
      -> Limited $ divSeq (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                       (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                                                 (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))
                                                           (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                          (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))
                                                     (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                         (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                                                                   (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                                  (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))
                                                                             (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                            (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))))))))))
                                               (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                   (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))
                                                                             (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                            (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o))))))))))
                                                                       (S (S (S (plus (plus (plus (plus o o) o) (S (plus (plus o o) o)))
                                                                                      (S (S (plus (plus (plus o o) o) (S (plus (plus o o) o)))))))))))))))))))))))
  IsLimited15 : (o : Nat)
    -> Limited $ divSeq (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus (plus o o)
                                                                                                                                                       (plus o o))
                                                                                                                                                 (plus (plus o o)
                                                                                                                                                       (plus o o)))
                                                                                                                                           (plus (plus (plus o o)
                                                                                                                                                       (plus o o))
                                                                                                                                                 (plus (plus o o)
                                                                                                                                                       (plus o o))))
                                                                                                                                     (plus (plus (plus (plus o o)
                                                                                                                                                       (plus o o))
                                                                                                                                                 (plus (plus o o)
                                                                                                                                                       (plus o o)))
                                                                                                                                           (plus (plus (plus o o)
                                                                                                                                                       (plus o o))
                                                                                                                                                 (plus (plus o o)
                                                                                                                                                       (plus o o)))))
                               (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus (plus o o)
                                                                         (plus o o))
                                                                   (plus (plus o o)
                                                                         (plus o o)))
                                                             (plus (plus (plus o o)
                                                                         (plus o o))
                                                                   (plus (plus o o)
                                                                         (plus o o))))
                                                       (plus (plus (plus (plus o o)
                                                                         (plus o o))
                                                                   (plus (plus o o)
                                                                         (plus o o)))
                                                             (plus (plus (plus o o)
                                                                         (plus o o))
                                                                   (plus (plus o o)
                                                                         (plus o o)))))))))))))))))))))))))))))))))))))
                           (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (S (plus (plus (plus (plus (plus o o)
                                                                   (plus o o))
                                                             (plus (plus o o)
                                                                   (plus o o)))
                                                       (plus (plus (plus o o)
                                                                   (plus o o))
                                                             (plus (plus o o)
                                                                   (plus o o))))
                                                 (plus (plus (plus (plus o o)
                                                                   (plus o o))
                                                             (plus (plus o o)
                                                                   (plus o o)))
                                                       (plus (plus (plus o o)
                                                                   (plus o o))
                                                             (plus (plus o o)
                                                                   (plus o o))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
      -> Limited $ divSeq (S (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                          (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))
                                                                    (S (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                      (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))))
                                                              (S (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o)))))))))))))
                                                        (S (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                               (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))
                                                                                         (S (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                                           (S (S (S (plus (plus (plus o o) o)
                                                                                                                          (S (S (plus (plus o o) o)))))))))))))
                                                                                   (S (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                                     (S (S (S (plus (plus (plus o o) o)
                                                                                                                    (S (S (plus (plus o o) o)))))))))))))))))))))
                                                  (S (S (S (S (S (S (S (plus (plus (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                         (S (S (S (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))))))
                                                                                   (S (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                                     (S (S (S (plus (plus (plus o o) o)
                                                                                                                    (S (S (plus (plus o o) o)))))))))))))
                                                                             (S (S (S (S (plus (plus (plus (plus o o) o) (S (S (plus (plus o o) o))))
                                                                                               (S (S (S (plus (plus (plus o o) o)
                                                                                                              (S (S (plus (plus o o) o))))))))))))))))))))))))))))

P : Nat -> Type
P n = Limited $ divSeq (n+n+n)
definiP : (n : Nat) -> P n = Limited $ divSeq (n+n+n)
definiP n = Refl

-- 無限降下法（の変形） Isabelleで証明した
postulate infiniteDescent0 :
  ((n:Nat) -> (Not . P) (S n) -> (m ** (LTE (S m) (S n), (Not . P) m)))
    -> P Z
      -> P n
-- ########################################



--            from ProofColDivSeqMain
-- ########################################
-- ########################################



--            from sub0xxxxx
-- ########################################
-- ########################################



