proposition: Theorem make_zop: forall (t:univ_of_cycles) (ops : ZnZ.Ops t), @ZnZ.to_Z _ (mk_zn2z_ops ops) = fun z => match z with | W0 => 0 | WW xh xl => ZnZ.to_Z xh * base (ZnZ.digits ops) + ZnZ.to_Z xl end.
proof: Proof. intros ww x; auto. Qed.
imports: ZArith Lia Ndigits BigNumPrelude DoubleType DoubleBase CyclicAxioms DoubleCyclic