fact: Fixpoint get_low (n : nat) {struct n}: word w n -> w := match n return (word w n -> w) with | 0%nat => fun x => x | S n1 => fun x => match x with | W0 => w_0 | WW _ x1 => get_low n1 x1 end end.
imports: ZArith Ndigits BigNumPrelude DoubleType