proposition: Lemma ldiff_alt x y p : 0 <= x < 2^p -> 0 <= y < 2^p -> Z.ldiff x y = Z.land x (Z.lxor y (2^p - 1)).
proof: Proof. intros (Hx,Hx') (Hy,Hy'). destruct p as [|p|p]. - simpl in *; replace x with 0; replace y with 0; auto with zarith. - rewrite <- Z.shiftl_1_l. change (_ - 1) with (Z.ones (Z.pos p)). rewrite <- Z.ldiff_ones_l_low; trivial. rewrite !Z.ldiff_land, Z.land_assoc. f_equal. rewrite Z.land_ones; try easy. symmetry. apply Z.mod_small; now split. Z.le_elim Hy. + now apply Z.log2_lt_pow2. + now subst. - simpl in *; lia. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen