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