proposition: Lemma spec_double_split : forall n x, let (h,l) := double_split n x in [!S n|x!] = [!n|h!] * double_wB n + [!n|l!].
proof: Proof. destruct x;simpl;auto. destruct n;simpl;trivial. rewrite spec_w_0;trivial. Qed.
imports: ZArith Ndigits BigNumPrelude DoubleType