binet's formula

Stream: new members

[Lawrence Lin]

hi guys!! i'm trying to divide both sides by x, but... i'm not sure how.

lemma binet_lemma (x : ℝ) (hx : x^2 = x + 1) (n : ℕ) (hn : n > 0) : x^n = x*(fib n) + fib (n-1) :=
begin
  cases n,
  { exfalso, linarith, },
  { induction n with n,
      { simp [fib], },
      {
        have H1 : x * ↑(fib (n + 1)) + ↑(fib n.succ) = (x + 1) * fib(n+1),
        { linarith, },
        rw [fib_rule],
        simp,
        rw [mul_add, add_assoc, H1, ←hx],
        by_cases x = 0,
        { exfalso, rw h at hx, linarith, },
        {

        },
      },
  },
end

that is, showing x ^ n.succ.succ = x * ↑(fib n) + x ^ 2 * ↑(fib (n + 1)) when divided by both sides with x gives the hypothesisn_ih

[Adam Topaz]

You can use tactic#apply_fun and apply the function which is division by x. You will then need to probe that this function is injevtive.

[Adam Topaz]

If you're looking for more detailed help, then a #mwe would be helpful

[Lawrence Lin]

how do i invent division?

[Junyan Xu]

I guess you can simply rw ← mul_left_inj' h
docs#mul_left_inj'