theorem WithZero.exists_ne_zero_and_lt {G : Type u_1} [LinearOrder G] [NoMinOrder G] {x : WithZero G} (hx : x ≠ 0) : ∃ (y : WithZero G), y ≠ 0 ∧ y < x

theorem WithZero.exists_ne_zero_and_le_and_le {G : Type u_1} [LinearOrder G] {x y : WithZero G} (hx : x ≠ 0) (hy : y ≠ 0) : ∃ (z : WithZero G), z ≠ 0 ∧ z ≤ x ∧ z ≤ y

theorem WithZero.exists_ne_zero_and_lt_and_lt {G : Type u_1} [LinearOrder G] [NoMinOrder G] {x y : WithZero G} (hx : x ≠ 0) (hy : y ≠ 0) : ∃ (z : WithZero G), z ≠ 0 ∧ z < x ∧ z < y