proposition: Lemma not_int_lor : forall a b, (not_int (a lor b) = (not_int a) land (not_int b))%uint63.
proof: Proof. intros. apply bit_ext'; intros. rewrite Uint63.land_spec. rewrite! bit_not_int by auto. rewrite Uint63.lor_spec. apply negb_orb. Qed.
imports: Bool ZifyClasses ZifyUint63 ZArith Lia Cdcl.PatriciaR