proposition: Lemma bit_add_or : forall x y : int, (forall n : int, bit x n = true -> bit y n = true -> False) -> (x + y)%uint63 = (x lor y)%uint63.
proof: Proof. intros. now apply Uint63.bit_add_or. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR