proposition: Lemma OMEGA4 x y z : x > 0 -> y > x -> z * y + x <> 0.
proof: Proof. Z.swap_greater. intros Hx Hxy. rewrite Z.add_move_0_l, <- Z.mul_opp_l. destruct (Z.lt_trichotomy (-z) 1) as [LT|[->|GT]]. - intro. revert LT. apply Z.le_ngt, (Z.le_succ_l 0). apply Z.mul_pos_cancel_r with y; Z.order. - Z.nzsimpl. Z.order. - rewrite (Z.mul_lt_mono_pos_r y), Z.mul_1_l in GT; Z.order. Qed.
imports: BinInt Znat