proposition: Lemma base_xO: forall n, base (xO n) = (base n)^2.
proof: Proof. intros n1; unfold base. rewrite (Pos2Z.inj_xO n1); rewrite Z.mul_comm; rewrite Z.pow_mul_r; auto with zarith. Qed.
imports: ZArith Lia Ndigits BigNumPrelude DoubleType DoubleBase CyclicAxioms DoubleCyclic