proposition: Lemma compare_refl : forall i, (i ?= i)%uint63 = Eq.
proof: Proof. intros. rewrite compare_def_spec. unfold compare_def. replace (i <? i)%uint63 with false by lia. replace (i =? i)%uint63 with true by lia. reflexivity. Qed.
imports: Bool ZifyBool ZArith ZifyUint63 Uint63 Lia List