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_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 α]
[PartialOrder α]
{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 α]
[PartialOrder α]
{a : α}
{b : α}
{c : α}
(ha : a ≠ 0)
(hb : b ≠ 0)
:
c ≠ 0