fact: Fixpoint eq_num (n1 n2: number) := match n1 with | nil => zerop_num n2 | a :: n3 => match n2 with | nil => zerop_num n1 | b :: n4 => match a ?= b with | Eq => eq_num n3 n4 | _ => false end end end.
imports: List ZArith Znumtheory Uint63 Cyclic63