fact: Fixpoint decr_num (n: number): number := match n with | nil => 1 :: nil | a :: n1 => match a ?= 0 with | Eq => max_int :: decr_num n1 | _ => (a - 1) :: n1 end end.
imports: List ZArith Znumtheory Uint63 Cyclic63