Dividing / multipling an inequality by a positive number

Stream: new members

[Michael Novak]

Suppose I proved a theorem which is some inequality about real numbers of the form a \leq b. how can I use the fact that if I multiply or divide both sides of this inequality by a positive number it's still true? For example if I want to use this inequality divided by 2 in another theorem I'm trying to prove.

[Notification Bot]

This topic was moved here from #lean4 > Dividing / Multipling a inequality by a positive number by Michael Novak.

[Yaël Dillies]

Do you know about the gcongr tactic?

[Michael Novak]

no

[Yaël Dillies]

It would be good if you had a MWE, but roughly if you do have : a / 2 ≤ b / 2 := by gcongr then you will left with a goal of ⊢ a ≤ b.

[Yaël Dillies]

Also in the future, please do not #lean4 for questions which are not related to developing the Lean programming language

[Michael Novak]

Oh sorry, I thought this is a channel for questions about using lean. Which channel is better for this sort of questions? And thank you very much for the suggestion of the gcongr tactic it looks like exactly what I was looking for. And lastly, what is a MWE ?

[Yaël Dillies]

You can use #general for questions which you expect will be interesting to read the answers to in several months, or #new members for more basic questions.

[Yaël Dillies]

You can click on the link to discover what a #mwe is

[Michael Rothgang]

Reading this thread, it seems to me that #**new members> would be appropriate for this one.

[Notification Bot]

This topic was moved here from #lean4 > Dividing / multipling an inequality by a positive number by Damiano Testa.