A bunch of dummy lemmas to be used in broken positivity extensions

The lack of pattern-matching in Qq means that we currently cannot write sound positivity extensions that work on non-generic nor concrete types (eg α → β). So for the time being we replace them by unsound ones using the following dummy lemmas.

We want to avoid

• breaking existing proofs
• accidentally making the proofs think they don't need some positivity assumption

theorem Mathlib.Meta.Positivity.dummy_pos {α : Type u_1} [Zero α] [PartialOrder α] {a : α} : 0 < a

theorem Mathlib.Meta.Positivity.dummy_nng {α : Type u_1} [Zero α] [PartialOrder α] {a : α} : 0 ≤ a

theorem Mathlib.Meta.Positivity.dummy_nzr {α : Type u_1} [Zero α] {a : α} : a ≠ 0

theorem Mathlib.Meta.Positivity.dummy_pos_of_pos {α : Type u_1} [Zero α] [PartialOrder α] {a : α} {b : α} (ha : 0 < a) : 0 < b

theorem Mathlib.Meta.Positivity.dummy_pos_of_nzr {α : Type u_1} [Zero α] [PartialOrder α] {a : α} {b : α} (ha : a ≠ 0) : 0 < b

theorem Mathlib.Meta.Positivity.dummy_nng_of_nng {α : Type u_1} [Zero α] [PartialOrder α] {a : α} {b : α} (ha : 0 ≤ a) : 0 ≤ b

theorem Mathlib.Meta.Positivity.dummy_nzr_of_nzr {α : Type u_1} [Zero α] {a : α} {b : α} (ha : a ≠ 0) : b ≠ 0

theorem Mathlib.Meta.Positivity.dummy_pos_of_pos_pos {α : Type u_1} [Zero α] [PartialOrder α] {a : α} {b : α} {c : α} (ha : 0 < a) (hb : 0 < b) : 0 < c

theorem Mathlib.Meta.Positivity.dummy_nng_of_pos_nng {α : Type u_1} [Zero α] [PartialOrder α] {a : α} {b : α} {c : α} (ha : 0 < a) (hb : 0 ≤ b) : 0 ≤ c

theorem Mathlib.Meta.Positivity.dummy_nng_of_nng_pos {α : Type u_1} [Zero α] [PartialOrder α] {a : α} {b : α} {c : α} (ha : 0 ≤ a) (hb : 0 < b) : 0 ≤ c

theorem Mathlib.Meta.Positivity.dummy_nng_of_nng_nng {α : Type u_1} [Zero α] [PartialOrder α] {a : α} {b : α} {c : α} (ha : 0 ≤ a) (hb : 0 ≤ b) : 0 ≤ c

theorem Mathlib.Meta.Positivity.dummy_nzr_of_pos_nzr {α : Type u_1} [Zero α] [PartialOrder α] {a : α} {b : α} {c : α} (ha : 0 < a) (hb : b ≠ 0) : c ≠ 0

theorem Mathlib.Meta.Positivity.dummy_nzr_of_nzr_pos {α : Type u_1} [Zero α] [PartialOrder α] {a : α} {b : α} {c : α} (ha : a ≠ 0) (hb : 0 < b) : c ≠ 0

theorem Mathlib.Meta.Positivity.dummy_nzr_of_nzr_nzr {α : Type u_1} [Zero α] {a : α} {b : α} {c : α} (ha : a ≠ 0) (hb : b ≠ 0) : c ≠ 0