have : (n-3) + 3 = n := by {
  sorry
}
P : ℕ → Prop
n : ℕ
h_3_le_n : 3 ≤ n
hftf : from_three_five (n - 3)
⊢ from_three_five n
P : ℕ → Prop
n : ℕ
h_3_le_n : 3 ≤ n
hftf : from_three_five (n - 3)
this : n - 3 + 3 = n
⊢ from_three_five n