proposition: Lemma digits_dom_op_incr : forall n m, (n<=m)%nat -> (ZnZ.digits (dom_op n) <= ZnZ.digits (dom_op m))%positive.
proof: Proof. intros. change (Zpos (ZnZ.digits (dom_op n)) <= Zpos (ZnZ.digits (dom_op m))). rewrite !digits_dom_op, !Pshiftl_nat_Zpower. apply Z.mul_le_mono_nonneg_l; auto with zarith. apply Z.pow_le_mono_r; auto with zarith. Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen