proposition: Lemma lxor_spec' x y : φ (x lxor y) = Z.lxor φ(x) φ(y).
proof: Proof. apply Z.bits_inj'; intros n hn. destruct (to_Z_bounded (x lxor y)) as [ hxy hxy' ]. destruct (to_Z_bounded x) as [ hx hx' ]. destruct (to_Z_bounded y) as [ hy hy' ]. case (Z_lt_le_dec n (φ digits)); intros hd. 2: { rewrite !Z.bits_above_log2; auto. - apply Z.lxor_nonneg; split; auto. - eapply Z.le_lt_trans. { apply Z.log2_lxor; assumption. } apply Z.max_lub_lt; apply (lt_pow_lt_log φ digits); split; assumption || reflexivity. - apply (lt_pow_lt_log φ digits); split; assumption || reflexivity. } rewrite (is_int n). { rewrite Z.lxor_spec, <- !bitE, lxor_spec; reflexivity. } apply (conj hn). apply (Z.lt_trans _ _ _ hd). apply Zpower2_lt_lin. lia. Qed.
imports: Utf8 DoubleType Lia Zpow_facts Zgcd_alt PrimInt63