fact: Fixpoint compare0_mn (n:nat) : word wm n -> comparison := match n return word wm n -> comparison with | O => compare0_m | S m => fun x => match x with | W0 => Eq | WW xh xl => match compare0_mn m xh with | Eq => compare0_mn m xl | _ => Lt end end end.
imports: ZArith Lia Ndigits BigNumPrelude DoubleType DoubleBase CyclicAxioms DoubleCyclic