fact: Definition double_WW (n:nat) := match n return word w n -> word w n -> word w (S n) with | O => w_WW | S n => fun (h l : zn2z (word w n)) => match h, l with | W0, W0 => W0 | _, _ => WW h l end end.
imports: ZArith Ndigits BigNumPrelude DoubleType