{R : Type u_1} →
  [inst : CommRing R] →
    {motive : ValuativeRel R → Sort u} →
      (t : ValuativeRel R) →
        ((vle : R → R → Prop) →
            (vle_total : ∀ (x y : R), vle x y ∨ vle y x) →
              (vle_trans : ∀ {z y x : R}, vle x y → vle y z → vle x z) →
                (vle_add : ∀ {x y z : R}, vle x z → vle y z → vle (x + y) z) →
                  (mul_vle_mul_left : ∀ {x y : R}, vle x y → ∀ (z : R), vle (x * z) (y * z)) →
                    (vle_mul_cancel : ∀ {x y z : R}, ¬vle z 0 → vle (x * z) (y * z) → vle x y) →
                      (not_vle_one_zero : ¬vle 1 0) →
                        motive
                          { vle := vle, vle_total := vle_total, vle_trans := vle_trans, vle_add := vle_add,
                            mul_vle_mul_left := mul_vle_mul_left, vle_mul_cancel := vle_mul_cancel,
                            not_vle_one_zero := not_vle_one_zero }) →
          motive t