Naming consistency around `if_pos`/`ite_pos`

Stream: mathlib4

[Emilie (Shad Amethyst)]

It seems odd to me that docs#if_pos is the equivalent of docs#if_true (in std4), but docs#ite_pos refers to the ordering of if-then-else.
On top of that, most of the lemmas around docs#ite_pos and docs#ite_le_one are only used in three files (the positivity tactic, Archive/Sensitivity.lean and Order/Pi.lean),
and they seem to me like they could easily be substituted with four much more general lemmas (plus four more for dite):

• ite_le : a ≤ x → b ≤ x → ite h a b ≤ x
• ite_lt : a < x → b < x → ite h a b < x
• le_ite : x ≤ a → x ≤ b → x ≤ ite h a b
• lt_ite

Removing ite_pos in favor of lt_ite & others would both remove the confusion about the meaning of pos in ite_pos and make those lemmas more general.
We could also use this opportunity to decide on a naming convention to stick to for if-then-else (if_xyz versus ite_xyz).

[Ruben Van de Velde]

We definitely want to keep the signature of if_pos if not the name

[Yaël Dillies]

Feel free to generalise ite_pos so long as the positivity extension still works

[Mario Carneiro]

I think if_true should be renamed to ite_true

[Kevin Buzzard]

How about \forall P, P a -> P b -> P (ite h a b) :-)