An example of a LinearOrderedCommMonoidWithZero in which the product of two positive elements vanishes.

This is the monoid with 3 elements 0, ε, 1 where ε ^ 2 = 0 and everything else is forced. The order is 0 < ε < 1. Since ε ^ 2 = 0, the product of strictly positive elements can vanish.

Relevant Zulip chat: https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/mul_pos

inductive Counterexample.Foo : Type

• zero: Counterexample.Foo
• eps: Counterexample.Foo
• one: Counterexample.Foo

The three element monoid.

instance Counterexample.instDecidableEqFoo : DecidableEq Counterexample.Foo

instance Counterexample.Foo.inhabited : Inhabited Counterexample.Foo

instance Counterexample.Foo.instZeroFoo : Zero Counterexample.Foo

instance Counterexample.Foo.instOneFoo : One Counterexample.Foo

def Counterexample.Foo.aux1 : Counterexample.Foo → ℕ

The order on Foo is the one induced by the natural order on the image of aux1.

def Counterexample.Foo.boom : Lean.ParserDescr

A tactic to prove facts by cases.

theorem Counterexample.Foo.aux1_inj : Function.Injective Counterexample.Foo.aux1

instance Counterexample.Foo.linearOrder : LinearOrder Counterexample.Foo

def Counterexample.Foo.mul : Counterexample.Foo → Counterexample.Foo → Counterexample.Foo

Multiplication on Foo: the only external input is that ε ^ 2 = 0.

instance Counterexample.Foo.commMonoid : CommMonoid Counterexample.Foo

instance Counterexample.Foo.instLinearOrderedCommMonoidWithZeroFoo : LinearOrderedCommMonoidWithZero Counterexample.Foo

theorem Counterexample.Foo.not_mul_pos : ¬∀ {M : Type} [inst : LinearOrderedCommMonoidWithZero M] (a b : M), 0 < a → 0 < b → 0 < a * b