Theorem: ftf_add_3_of_ftf_self (BrownCs22/Homework/Hw9.lean)

State before:
P : ℕ → Prop
n : ℕ
⊢ from_three_five n → from_three_five (n + 3)
Tactic:
sorry
State after:
no goals