proposition: Lemma spec_double_WW : forall n (h l : word w n), [!S n|double_WW n h l!] = [!n|h!] * double_wB n + [!n|l!].
proof: Proof. induction n;simpl;intros;trivial. destruct h;auto. destruct l;auto. Qed.
imports: ZArith Ndigits BigNumPrelude DoubleType