two_mul_add_one_iff_not_odd.lean

lemma nat.dvd_sub_of_mod_eq {a b c : ℕ} (h : a % b = c) : b ∣ a - c :=
begin
  have : c ≤ a,
  { rw ←h, exact nat.mod_le a b },
  rw [←int.coe_nat_dvd, int.coe_nat_sub this],
  apply int.dvd_sub_of_mod_eq,
  rw ←int.coe_nat_mod, rw h,
end

theorem nat.one_le_of_not_even {n : ℕ} (h : ¬n.even) : 1 ≤ n :=
begin
  apply nat.succ_le_of_lt,
  rw nat.pos_iff_ne_zero,
  rintro rfl,
  exact h nat.even_zero
end

lemma two_mul_add_one_iff_not_odd (n : ℕ) : ¬n.even ↔ ∃ m, n = 2 * m + 1 :=
begin
  split; intro h,
  { have hn : 1 ≤ n := nat.one_le_of_not_even h,
    rw nat.not_even_iff at h,
    obtain ⟨m, hm⟩ := nat.dvd_sub_of_mod_eq h,
    use m,
    rw [←hm, nat.sub_add_cancel hn] },
  { obtain ⟨m, hm⟩ := h,
    rw hm,
    apply nat.two_not_dvd_two_mul_add_one }
end