proposition: Theorem Zpos_pos: forall x, 0 < Zpos x.
proof: Proof. red; simpl; auto. Qed.
imports: Bignums(DoubleBase DoubleSub DoubleMul DoubleSqrt DoubleLift DoubleDivn1 DoubleDiv) Bignums(DoubleCyclic BigN) CyclicAxioms Cyclic63 ZArith ZCAux