∀ {α : Type u_2} {β : Type u_3} {inst : AddCommMonoid α} {inst_1 : PartialOrder α} {inst_2 : AddCommMonoid β}
  {inst_3 : PartialOrder β} {inst_4 : SMulZeroClass α β} [self : FloorDiv α β] ⦃a : α⦄,
  0 < a → GaloisConnection (fun x => a • x) fun x => x ⌊/⌋ a