proposition: Theorem spec_ldiff x y : [ldiff x y] = Z.ldiff [x] [y].
proof: Proof. rewrite ldiff_fold. apply spec_same_level; clear x y. intros n x y. simpl. rewrite spec_reduce. rewrite ZnZ.spec_land, ZnZ.spec_lxor, ZnZ.spec_m1. symmetry. apply ldiff_alt; apply ZnZ.spec_to_Z. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen