proposition: Theorem spec_lor x y : [lor x y] = Z.lor [x] [y].
proof: Proof. rewrite lor_fold. apply spec_same_level; clear x y. intros n x y. simpl. rewrite spec_reduce. apply ZnZ.spec_lor. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen