DEFINITION arith0()
TYPE =
       ∀h2:nat
         .∀d2:nat
           .∀n:nat.(le (plus d2 h2) n)→∀h1:nat.(le (plus d2 h1) (minus (plus n h1) h2))
BODY =
        assume h2: nat
        assume d2: nat
        assume n: nat
        suppose H: le (plus d2 h2) n
        assume h1: nat
          by (minus_plus . .)
          we proved eq nat (minus (plus h2 (plus d2 h1)) h2) (plus d2 h1)
          we proceed by induction on the previous result to prove le (plus d2 h1) (minus (plus n h1) h2)
             case refl_equal : ⇒
                the thesis becomes le (minus (plus h2 (plus d2 h1)) h2) (minus (plus n h1) h2)
                   (h1) 
                      by (le_plus_l . .)
le h2 (plus h2 (plus d2 h1))
                   end of h1
                   (h2) 
                      (h1) 
                         (h1) 
                            by (le_n .)
                            we proved le h1 h1
                            by (le_plus_plus . . . . H previous)
                            we proved le (plus (plus d2 h2) h1) (plus n h1)
                            by (le_n_S . . previous)
                            we proved le (S (plus (plus d2 h2) h1)) (S (plus n h1))
                            by (le_S_n . . previous)
le (plus (plus d2 h2) h1) (plus n h1)
                         end of h1
                         (h2) 
                            by (plus_sym . .)
eq nat (plus h2 d2) (plus d2 h2)
                         end of h2
                         by (eq_ind_r . . . h1 . h2)
le (plus (plus h2 d2) h1) (plus n h1)
                      end of h1
                      (h2) 
                         by (plus_assoc_l . . .)
eq nat (plus h2 (plus d2 h1)) (plus (plus h2 d2) h1)
                      end of h2
                      by (eq_ind_r . . . h1 . h2)
le (plus h2 (plus d2 h1)) (plus n h1)
                   end of h2
                   by (le_minus_minus . . h1 . h2)
le (minus (plus h2 (plus d2 h1)) h2) (minus (plus n h1) h2)
          we proved le (plus d2 h1) (minus (plus n h1) h2)
       we proved 
          ∀h2:nat
            .∀d2:nat
              .∀n:nat.(le (plus d2 h2) n)→∀h1:nat.(le (plus d2 h1) (minus (plus n h1) h2))