A simple Galois connection.

galois.lean

import tactic

@[simp] def f (x : ℕ) : ℕ := x * 2

@[simp] def g (x : ℕ) : ℕ := x / 2

@[simp] lemma nat.mul_two_div_two (n : ℕ) : (n * 2) / 2 = n :=
by { induction n; simp }

#check nat.le_div_iff_mul_le

example (n m : ℕ) : f n ≤ m ↔ n ≤ g m :=
begin
  unfold f g,
  revert n,
  apply nat.strong_induction_on m, clear m,
  intros m ih n,
  cases n,
  { simp },
  { cases lt_or_ge m 2 with h h,
    { simp [nat.div_eq_of_lt h, nat.succ_ne_zero, nat.succ_mul],
      linarith },
    { rw [nat.div_eq_sub_div two_pos h,
          ←nat.add_one,
          nat.add_le_add_iff_le_right,
          ←ih _ (nat.sub_lt_of_pos_le _ _ two_pos h) n,
          nat.add_one,
          nat.succ_mul,
          nat.add_le_to_le_sub _ h] } }
end