proposition: Lemma OMEGA19 x : Zne x 0 -> 0 <= x + -1 \/ 0 <= x * -1 + -1.
proof: Proof. unfold Zne. intros Hx. apply Z.lt_gt_cases in Hx. destruct Hx as [LT|GT]. - right. change (-1) with (-(1)). rewrite Z.mul_opp_r, <- Z.opp_add_distr. Z.nzsimpl. rewrite Z.opp_nonneg_nonpos. now apply Z.le_succ_l. - left. now apply Z.lt_le_pred. Qed.
imports: BinInt Znat