import Mathlib.Data.Nat.Basic
import Mathlib.Tactic

namespace Goppadecoding

section lemmas_nat

theorem sub_one_lt_if_one_le {n: ℕ} (n1: 1 ≤ n)
: (n-1:ℕ) < n :=
by
  apply Nat.sub_lt_of_pos_le 1 n
  simp only
  exact n1

theorem dbl_sub_one_add_one_eq_dbl_if_one_le {n: ℕ} (n1: 1 ≤ n)
: (2*n-1:ℕ)+1 = 2*n :=
by
  apply tsub_add_cancel_of_le
  calc
    1 ≤ 2*1 := by norm_num
    _ ≤ 2*n := Nat.mul_le_mul_left 2 n1

theorem sub_one_add_eq_dbl_sub_one {n: ℕ}
: (n-1:ℕ)+n = (2*n-1:ℕ) :=
by
  by_cases n0: n = 0
  . rw[n0]
  have n1: 1 ≤ n := Nat.one_le_iff_ne_zero.mpr n0
  calc
    _ = (n+n-1:ℕ) := tsub_add_eq_add_tsub n1
    _ = (2*n-1:ℕ) := by rw[Nat.two_mul]

theorem ge_1_if_odd {n: ℕ}:
  Odd n → 1 ≤ n :=
by
  contrapose
  intro n1
  simp only [not_le, Nat.lt_one_iff] at n1
  rw[n1]
  norm_num

theorem eq_if_bounded_bounded_eqflip {d i j: ℕ}:
  i < d → j < d → d-1-i = d-1-j → i = j :=
by
  intro id jd d1id1j
  have id1: i ≤ d-1 := Nat.le_pred_of_lt id
  have jd1: j ≤ d-1 := Nat.le_pred_of_lt jd
  have ix: d-1-(d-1-i) = i := Nat.sub_sub_self id1
  have jx: d-1-(d-1-j) = j := Nat.sub_sub_self jd1
  simp_all only

theorem half_times_2_eq_not_even_1 (n: ℕ):
  ¬Even n → ((n-1) / 2) * 2 = n-1 :=
by
  intro odd
  rw[Nat.even_iff_not_odd] at odd
  simp only[not_not] at odd
  have nge1: 1 ≤ n := ge_1_if_odd odd
  have even1: Even (n-1) := by
    rw[Nat.even_sub' nge1]
    simp only[odd]
  apply Nat.div_two_mul_two_of_even even1

theorem fin_nat_sub_eq_sub {m: ℕ} {n: ℕ} [NeZero n] {x: Fin n} (mx: m ≤ (x:ℕ)):
  (((x:ℕ)-m:ℕ): Fin n) = x-m :=
by
  let y:ℕ := (x:ℕ) - m
  have ym: y+m = (x:ℕ) := Nat.sub_add_cancel mx
  have xym: (x:ℕ) = y+m := Eq.symm ym
  have xx: x = (x:ℕ) := Eq.symm (Fin.cast_val_eq_self x)
  rw[xym,xx,xym]
  simp only [ge_iff_le, add_le_iff_nonpos_left, nonpos_iff_eq_zero, tsub_eq_zero_iff_le, add_tsub_cancel_right, Nat.cast_add, add_sub_cancel]

theorem le_add_self_if_le {x y: WithBot ℕ}:
  0 ≤ x → y ≤ x+y :=
by apply le_add_of_nonneg_left

theorem lt_if_nat_add_lt {y z: WithBot ℕ} {x: ℕ}:
  x+y < z → y < z :=
by
  intro xyz
  have x0: 0 ≤ (x:WithBot ℕ) := Nat.WithBot.coe_nonneg
  have yxy: y ≤ x+y := le_add_self_if_le x0
  exact lt_of_le_of_lt yxy xyz

theorem add_left_nat_lt_if_lt (x: ℕ) {y z: WithBot ℕ}:
  y < z → x+y < x+z :=
by
  intro yz
  have znotbot: z ≠ ⊥ := ne_bot_of_gt yz
  have znat: z.unbot znotbot = z := z.coe_unbot znotbot
  have xz: (x+(z.unbot znotbot):ℕ) = x+z := Mathlib.Tactic.Ring.inv_add rfl znat
  rw[← xz]
  by_cases ybot: y = ⊥
  . rw[ybot,WithBot.add_bot]
    apply WithBot.bot_lt_coe
  have ynotbot: y ≠ ⊥ := ybot
  have ynat: y.unbot ynotbot = y := y.coe_unbot ynotbot
  have xy: (x+(y.unbot ynotbot):ℕ) = x+y := Mathlib.Tactic.Ring.inv_add rfl ynat
  have yz2: (y.unbot ynotbot:WithBot ℕ) < z.unbot znotbot := by
    rw[ynat,znat]
    exact yz
  have yz3: y.unbot ynotbot < z.unbot znotbot := WithBot.coe_lt_coe.mp yz2
  rw[← xy]
  norm_cast
  exact Nat.add_lt_add_left yz3 x

theorem le_sub_one_if_one_le_and_add_one_le {x: WithBot ℕ} {y: ℕ}
  (y1: 1 ≤ y) (x1y: x+1 ≤ y)
: x ≤ (y-1:ℕ) :=
by
  by_cases xbot: x = ⊥
  . rw[xbot]
    exact bot_le
  let n := x.unbot xbot
  have nx: n = x := x.coe_unbot xbot
  rw[← nx]
  norm_cast
  apply (le_tsub_iff_right y1).mpr
  rw[← nx] at x1y
  norm_cast at x1y

end lemmas_nat