fact: Fixpoint compare_mn_1 (n:nat) : word wm n -> w -> comparison := match n return word wm n -> w -> comparison with | 0 => compare_m | S m => fun x y => match x with | W0 => compare w_0 y | WW xh xl => match compare0_mn m xh with | Eq => compare_mn_1 m xl y | r => Gt end end end.
imports: ZArith Basic_type