proposition: Theorem branching_bit_spec: forall k1 k2, k1 <> k2 -> exists n, is_mask (branching_bit k1 k2) n /\ (forall p, (p < n)%nat -> testbit k1 p = testbit k2 p) /\ (testbit k1 n <> testbit k2 n).
proof: Proof. intros. unfold branching_bit. destruct (eqb_dec (lxor k1 k2) zero). { elim H; apply lxor_eq_zero; auto. } { generalize (lowest_bit_spec _ n). intros [r [HA HB]]. exists r; split; auto. split. - intros. apply xorb_eq. rewrite <- lxor_spec. apply HB; auto. - assert (testbit (lowest_bit (lxor k1 k2)) r = true) by (apply HA; auto). unfold lowest_bit in H0. rewrite land_spec in H0. rewrite lxor_spec in H0. red; intros. unfold testbit in H1. rewrite H1 in H0. rewrite xorb_nilpotent in H0. simpl in H0. inv H0. } Qed.
imports: Lia Cdcl.Coqlib