hpastetwo

foo = 
fun x : nat =>
nat_ind
  (fun x0 : nat => forall y j k : nat, x0 < j -> y < k -> x0 * y < j * k)
  (fun y j : nat =>
   match j as n return (forall k : nat, 0 < n -> y < k -> 0 * y < n * k) with
   | 0 => fun (k : nat) (H : 0 < 0) (_ : y < k) => H
   | S j0 =>
       fun k : nat =>
       match k as n return (0 < S j0 -> y < n -> 0 < n + j0 * n) with
       | 0 =>
           fun (_ : 0 < S j0) (H0 : y < 0) =>
           le_plus_trans 1 0 (j0 * 0)
             (gt_le_S 0 0
                (False_ind (0 < 0)
                   (let H1 := H0 in
                    (let H2 := lt_n_O y in fun H3 : y < 0 => H2 H3) H1)))
       | S k0 =>
           fun (_ : 0 < S j0) (_ : y < S k0) =>
           le_plus_trans 1 (S k0) (j0 * S k0) (gt_le_S 0 (S k0) (lt_O_Sn k0))
       end
   end)
  (fun (x0 : nat)
     (IHx : forall y j k : nat, x0 < j -> y < k -> x0 * y < j * k)
     (y j : nat) =>
   match
     j as n return (forall k : nat, S x0 < n -> y < k -> S x0 * y < n * k)
   with
   | 0 =>
       fun (k : nat) (H : S x0 < 0) (_ : y < k) =>
       gt_le_S (y + x0 * y) 0
         (False_ind (S (y + x0 * y) <= 0)
            (let H1 := H in
             (let H2 := lt_n_O (S x0) in fun H3 : S x0 < 0 => H2 H3) H1))
   | S j0 =>
       fun (k : nat) (H : S x0 < S j0) (H0 : y < k) =>
       plus_lt_compat y k (x0 * y) (j0 * k) H0
         (IHx y j0 k (le_S_n (S x0) j0 H) H0)
   end) x
     : forall x y j k : nat, x < j -> y < k -> x * y < j * k