Assume H20: two_thirds = 0.

We prove the intermediate claim H0lt0: 0 < 0.

rewrite the current goal using H20 (from right to left) at position 2.

An exact proof term for the current goal is two_thirds_pos.

An exact proof term for the current goal is ((SNoLt_irref 0) H0lt0).

∎