proposition: Lemma eqb_spec : forall k1 k2, Uint63.eqb k1 k2 = true <-> k1 = k2.
proof: Proof. split ; intros. apply Uint63.eqb_correct; auto. apply Uint63.eqb_complete; auto. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR