use of pow_two_pos_of_ne_zero

Stream: general

[Jayden Vap]

I am attempting to finish the base case of an inductive proof, and in the current #mwe below, the goal is 0<x^2. I am curious if theres a way I can use pow_two_pos_of_ne_zero

theorem  inductionProblemV1
 (m: ℕ) (x: ℝ) (hn: m >=0) (h1x: x >-1)(h2x: x ≠ 0): (1+x)^(m+2)> 1 + (m+2)*x :=
begin
induction m with d hd,
repeat {rw zero_add},
simp,
rw add_pow_two,
rw mul_one,
rw one_pow,
simp,
pow_two_pos_of_ne_zero,

end

[Bryan Gin-ge Chen]

pos_two_pos_of_ne_zero is a term, not a tactic. In tactic mode you need to use something like tactic#exact, tactic#apply, or tactic#refine.

[Jayden Vap]

Okay, I will try that, thank you very much!

[Kevin Buzzard]

Can you edit your code block to include all imports, ie actually make it a #mwe (the link explains the things we hope for)

[Kevin Buzzard]

It's ok not to include imports in later discussions but you've started a new thread (which is fine) and the first piece of code on a new thread is supposed to be mwe and in particular it's supposed to work for anyone who just cuts and pastes it directly into lean

[Kevin Buzzard]

By the way, if you're faced with a goal like 0<x^2 and you feel confident that something like this should be in the library, you can try library_search which Is a tactic which might close your goal automatically