proposition: Theorem Zcompare_spec : forall x y, Zcompare_prop x y (Z.compare x y).
proof: Proof. intros x y. destruct (Z_dec x y) as [[H|H]|H]. generalize (Zlt_compare _ _ H). case (Z.compare x y) ; try easy. now constructor. generalize (Zgt_compare _ _ H). case (Z.compare x y) ; try easy. constructor. now apply Z.gt_lt. generalize (proj2 (Zcompare_Eq_iff_eq _ _) H). case (Z.compare x y) ; try easy. now constructor. Qed.
imports: Coq(ZArith Lia Zquot)