proposition: Lemma head0_zdigits : forall n (x : dom_t n), 0 < ZnZ.to_Z x -> ZnZ.to_Z (ZnZ.head0 x) < ZnZ.to_Z (ZnZ.zdigits (dom_op n)).
proof: Proof. intros n x H. destruct (ZnZ.spec_head0 x H) as (_,H0). intros. assert (H1 := ZnZ.spec_to_Z (ZnZ.head0 x)). assert (H2 := ZnZ.spec_to_Z (ZnZ.zdigits (dom_op n))). unfold base in *. rewrite ZnZ.spec_zdigits in H2 |- *. set (h := ZnZ.to_Z (ZnZ.head0 x)) in *; clearbody h. set (d := ZnZ.digits (dom_op n)) in *; clearbody d. destruct (Z_lt_le_dec h (Zpos d)); auto. exfalso. assert (1 * 2^Zpos d <= ZnZ.to_Z x * 2^h). apply Z.mul_le_mono_nonneg; auto with zarith. apply Z.pow_le_mono_r; auto with zarith. rewrite Z.mul_comm in H0. auto with zarith. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen