proposition: Lemma compare_spec x y : compare x y = (φ x ?= φ y)%Z.
proof: Proof. rewrite compare_def_spec; unfold compare_def. case ltbP; [ auto using Z.compare_lt_iff | intros hge ]. case eqbP; [ now symmetry; apply Z.compare_eq_iff | intros hne ]. symmetry; apply Z.compare_gt_iff; lia. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63