{G : Type u_3} →
  {P : Type u_4} →
    [inst : LE G] →
      [inst_1 : LE P] →
        [inst_2 : VAdd G P] →
          {motive : IsOrderedCancelVAdd G P → Sort u} →
            (t : IsOrderedCancelVAdd G P) →
              ([toIsOrderedVAdd : IsOrderedVAdd G P] →
                  (le_of_vadd_le_vadd_left : ∀ (a : G) (b c : P), a +ᵥ b ≤ a +ᵥ c → b ≤ c) →
                    (le_of_vadd_le_vadd_right : ∀ (a b : G) (c : P), a +ᵥ c ≤ b +ᵥ c → a ≤ b) → motive ⋯) →
                motive t