proposition: Lemma lxor_eq_zero: forall k1 k2, lxor k1 k2 = zero -> k1 = k2.
proof: Proof. intros; eapply testbit_spec; intros. assert (testbit (lxor k1 k2) n = false) by (rewrite H; rewrite zero_spec; auto). rewrite lxor_spec in H0. apply xorb_eq; auto. Qed.
imports: Lia Cdcl.Coqlib