## Stream: new members

### Topic: Squaring an inequality?

#### James Arthur (Aug 15 2020 at 14:07):

As part of a larger proof, inverse hyperbolic trig, I have the following lemma. Basically I want to square both sides, but I don't think thats mathematically possible? Does lean have a little thing that makes this simpler?

lemma b_lt_sqrt_b_sq_add_one (b : ℝ) : b < sqrt(b ^ 2 + 1) :=
begin
-- I want to square this, but I don't think thats possible.
-- then do linaarith
sorry
end


#### Reid Barton (Aug 15 2020 at 14:08):

You want to find a lemma that says (under some side conditions) a < b <-> a^2 < b^2 (or maybe a*a < b*b)

#### James Arthur (Aug 15 2020 at 14:11):

I've just found apply mul_self_lt_mul_self_iff

#### James Arthur (Aug 15 2020 at 14:13):

However, my main lemma is sinh_surjective which just said sinh is surjective and thats not only for positives, the lemma is true for all x.

#### Kevin Buzzard (Aug 15 2020 at 14:31):

Then you should split into two cases b<=0 and b>0

#### James Arthur (Aug 15 2020 at 15:23):

Thankyou, splitting seemed to be the answer

#### Kenny Lau (Aug 15 2020 at 17:15):

b \le abs b = sqrt (b ^ 2) < sqrt (b ^ 2 + 1) is the answer @James Arthur

#### James Arthur (Aug 15 2020 at 17:32):

For reference, here is the code that I ended up using:

lemma b_lt_sqrt_b_sq_add_one ( b : ℝ) : b < sqrt(b^2 + 1) :=
begin
by_cases hb : 0 ≤ b,
conv {to_lhs, rw ← sqrt_sqr hb},
rw sqrt_lt,
linarith,
apply pow_two_nonneg,
have F : 0 ≤ b^2 := by {apply pow_two_nonneg},
linarith,
rw not_le at hb,
apply lt_of_lt_of_le hb,
apply sqrt_nonneg,
end


#### James Arthur (Aug 15 2020 at 17:32):

with help from @Shing Tak Lam

Last updated: May 13 2021 at 20:13 UTC