proposition: Lemma pow2_pos_minus_1 : forall z, 0<z -> 2^(z-1) = 2^z / 2.
proof: Proof. intros. apply Zdiv_unique with 0; auto with zarith. change 2 with (2^1) at 2. rewrite <- Zpower_exp; auto with zarith. rewrite Z.add_0_r. f_equal. auto with zarith. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen