{α : Type u_2} →
  {β : Type u_3} →
    [inst : AddCommMonoid α] →
      [inst_1 : PartialOrder α] →
        [inst_2 : AddCommMonoid β] →
          [inst_3 : PartialOrder β] →
            [inst_4 : SMulZeroClass α β] →
              {motive : FloorDiv α β → Sort u} →
                (t : FloorDiv α β) →
                  ((floorDiv : β → α → β) →
                      (floorDiv_gc : ∀ ⦃a : α⦄, 0 < a → GaloisConnection (fun x => a • x) fun x => floorDiv x a) →
                        (floorDiv_nonpos : ∀ ⦃a : α⦄, a ≤ 0 → ∀ (b : β), floorDiv b a = 0) →
                          (zero_floorDiv : ∀ (a : α), floorDiv 0 a = 0) →
                            motive
                              { floorDiv := floorDiv, floorDiv_gc := floorDiv_gc, floorDiv_nonpos := floorDiv_nonpos,
                                zero_floorDiv := zero_floorDiv }) →
                    motive t