DEFINITION leq_leqz()
TYPE =
       ∀a1:A.∀a2:A.(leqz a1 a2)→(leq gz a1 a2)
BODY =
        assume a1: A
        assume a2: A
        suppose H: leqz a1 a2
          we proceed by induction on H to prove leq gz a1 a2
             case leqz_sort : h1:nat h2:nat n1:nat n2:nat H0:eq nat (plus h1 n2) (plus h2 n1) ⇒
                the thesis becomes leq gz (ASort h1 n1) (ASort h2 n2)
                   (h1) 
                      (h1) 
                         (h1) 
                            (h1) 
                               (h1) 
                                  (h1) 
                                     (h1) 
                                        (h1) 
                                           by (sym_eq . . . H0)
                                           we proved eq nat (plus h2 n1) (plus h1 n2)
                                           by (f_equal . . . . . previous)
eq A (ASort O (plus h2 n1)) (ASort O (plus h1 n2))
                                        end of h1
                                        (h2) 
                                           by (next_plus_gz . .)
eq nat (next_plus gz n2 h1) (plus h1 n2)
                                        end of h2
                                        by (eq_ind_r . . . h1 . h2)
eq A (ASort O (plus h2 n1)) (ASort O (next_plus gz n2 h1))
                                     end of h1
                                     (h2) 
                                        by (next_plus_gz . .)
eq nat (next_plus gz n1 h2) (plus h2 n1)
                                     end of h2
                                     by (eq_ind_r . . . h1 . h2)
eq A (ASort O (next_plus gz n1 h2)) (ASort O (next_plus gz n2 h1))
                                  end of h1
                                  (h2) 
                                     by (le_plus_r . .)
                                     we proved le h2 (plus h1 h2)
                                     by (O_minus . . previous)
eq nat (minus h2 (plus h1 h2)) O
                                  end of h2
                                  by (eq_ind_r . . . h1 . h2)

                                     eq
                                       A
                                       ASort O (next_plus gz n1 h2)
                                       ASort (minus h2 (plus h1 h2)) (next_plus gz n2 h1)
                               end of h1
                               (h2) 
                                  by (le_plus_l . .)
                                  we proved le h1 (plus h1 h2)
                                  by (O_minus . . previous)
eq nat (minus h1 (plus h1 h2)) O
                               end of h2
                               by (eq_ind_r . . . h1 . h2)

                                  eq
                                    A
                                    ASort (minus h1 (plus h1 h2)) (next_plus gz n1 h2)
                                    ASort (minus h2 (plus h1 h2)) (next_plus gz n2 h1)
                            end of h1
                            (h2) 
                               by (minus_plus_r . .)
eq nat (minus (plus h1 h2) h2) h1
                            end of h2
                            by (eq_ind_r . . . h1 . h2)

                               eq
                                 A
                                 ASort (minus h1 (plus h1 h2)) (next_plus gz n1 h2)
                                 ASort (minus h2 (plus h1 h2)) (next_plus gz n2 (minus (plus h1 h2) h2))
                         end of h1
                         (h2) 
                            by (minus_plus . .)
eq nat (minus (plus h1 h2) h1) h2
                         end of h2
                         by (eq_ind_r . . . h1 . h2)

                            eq
                              A
                              ASort (minus h1 (plus h1 h2)) (next_plus gz n1 (minus (plus h1 h2) h1))
                              ASort (minus h2 (plus h1 h2)) (next_plus gz n2 (minus (plus h1 h2) h2))
                      end of h1
                      (h2) 
                         by (aplus_asort_simpl . . . .)

                            eq
                              A
                              aplus gz (ASort h2 n2) (plus h1 h2)
                              ASort (minus h2 (plus h1 h2)) (next_plus gz n2 (minus (plus h1 h2) h2))
                      end of h2
                      by (eq_ind_r . . . h1 . h2)

                         eq
                           A
                           ASort (minus h1 (plus h1 h2)) (next_plus gz n1 (minus (plus h1 h2) h1))
                           aplus gz (ASort h2 n2) (plus h1 h2)
                   end of h1
                   (h2) 
                      by (aplus_asort_simpl . . . .)

                         eq
                           A
                           aplus gz (ASort h1 n1) (plus h1 h2)
                           ASort (minus h1 (plus h1 h2)) (next_plus gz n1 (minus (plus h1 h2) h1))
                   end of h2
                   by (eq_ind_r . . . h1 . h2)
                   we proved 
                      eq
                        A
                        aplus gz (ASort h1 n1) (plus h1 h2)
                        aplus gz (ASort h2 n2) (plus h1 h2)
                   by (leq_sort . . . . . . previous)
leq gz (ASort h1 n1) (ASort h2 n2)
             case leqz_head : a0:A a3:A :leqz a0 a3 a4:A a5:A :leqz a4 a5 ⇒
                the thesis becomes leq gz (AHead a0 a4) (AHead a3 a5)
                (H1) by induction hypothesis we know leq gz a0 a3
                (H3) by induction hypothesis we know leq gz a4 a5
                   by (leq_head . . . H1 . . H3)
leq gz (AHead a0 a4) (AHead a3 a5)
          we proved leq gz a1 a2
       we proved ∀a1:A.∀a2:A.(leqz a1 a2)→(leq gz a1 a2)