∀ (motive : (x : ℕ) → (x_1 x_2 : Num) → x_1 ≤ x_2 → (x_1 * x_2).natSize ≤ x → Prop) (x : ℕ) (x_1 x_2 : Num)
  (x_3 : x_1 ≤ x_2) (x_4 : (x_1 * x_2).natSize ≤ x),
  (∀ (x : Num) (_ab : 0 ≤ x) (_h : (0 * x).natSize ≤ 0), motive 0 Num.zero x _ab _h) →
    (∀ (a : PosNum) (ab : Num.pos a ≤ 0) (_h : (Num.pos a * 0).natSize ≤ 0), motive 0 (Num.pos a) Num.zero ab _h) →
      (∀ (a a_1 : PosNum) (_ab : Num.pos a ≤ Num.pos a_1) (h : (Num.pos a * Num.pos a_1).natSize ≤ 0),
          motive 0 (Num.pos a) (Num.pos a_1) _ab h) →
        (∀ (n : ℕ) (x : Num) (_ab : 0 ≤ x) (_h : (0 * x).natSize ≤ n.succ), motive n.succ Num.zero x _ab _h) →
          (∀ (n : ℕ) (a : PosNum) (b : Num) (ab : Num.pos a ≤ b) (h : (Num.pos a * b).natSize ≤ n.succ),
              motive n.succ (Num.pos a) b ab h) →
            motive x x_1 x_2 x_3 x_4