proposition: Lemma spec_WO : forall h, zn2z_to_Z wB to_Z (WO h) = (to_Z h)*wB.
proof: Proof. unfold zn2z_to_Z, WO; simpl; intros. case_eq (eq0 h); intros. - rewrite (spec_eq0 _ H); auto. - rewrite spec_0; auto with zarith. Qed.
imports: ZArith Lia Znumtheory Zpow_facts DoubleType