proposition: Lemma eqb_eq : forall x y, eqb x y = true <-> x == y.
proof: Proof. intros. unfold eqb, eq. rewrite ZnZ.spec_compare. case Z.compare_spec; split; (easy || lia). Qed.
imports: ZArith Lia Znumtheory Zpow_facts DoubleType