proposition: Theorem cmk_op_digits: forall n, (Zpos (ZnZ.digits (cmk_op n)) = 2 ^ (Z_of_nat n) * 63)%Z.
proof: Proof. do 15 (intros n; case n; clear n; [try reflexivity | idtac]). intros n; unfold cmk_op; lazy beta. rewrite mk_op_digits; auto. Qed.
imports: CyclicAxioms Cyclic63 Int63Compat Bignums(DoubleCyclic BigN) ZArith ZCAux Mod_op