fact: Fixpoint incr_num (n: number): number := match n with | nil => 1 :: nil | a::n1 => let c := 1 + a in match c ?= 0 with | Eq => 0 :: incr_num n1 | _ => c :: n1 end end.
imports: List ZArith Znumtheory Uint63 Cyclic63