proposition: Lemma Zcompare_spec : forall x y, (x = y -> ZcompareZ x y = 0) /\ (x > y -> ZcompareZ x y = 1) /\ (x < y -> ZcompareZ x y = -1).
proof: Proof. unfold ZcompareZ. intros. destruct (x ?= y) eqn:C; simpl. - rewrite Z.compare_eq_iff in C. lia. - rewrite Z.compare_lt_iff in C. lia. - rewrite Z.compare_gt_iff in C. lia. Qed.
imports: Bool ZArith Zify ZifyClasses Lia