proposition: Theorem spec_tail0: forall x, 0 < [x] -> exists y, 0 <= y /\ [x] = (2 * y + 1) * 2 ^ [tail0 x].
proof: Proof. intros x. rewrite tail0_fold. destr_t x as (n,x). exact (ZnZ.spec_tail0 x). Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen