proposition: Lemma compare_Eq : forall x y, (x ?= y)%uint63 = Eq <-> (x =? y = true)%uint63.
proof: Proof. intros. rewrite compare_def_spec. unfold compare_def. destruct (x <?y)%uint63 eqn:LT; try congruence. intuition (congruence || lia). destruct (x =?y)%uint63 ; intuition (congruence || lia). Qed.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List