fact: Definition double_split (n:nat) (x:zn2z (word w n)) := match x with | W0 => match n return word w n * word w n with | O => (w_0,w_0) | S _ => (W0, W0) end | WW h l => (h,l) end.
imports: ZArith Ndigits BigNumPrelude DoubleType