proposition: Lemma spec_div2: forall x, [div2 x] = Z.div2 [x].
proof: Proof. intros. unfold div2. symmetry. rewrite spec_shiftr, spec_1. apply Z.div2_spec. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen