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