fact: Fixpoint cpr_num (n1 n2: number) res := match n1 with | nil => if zerop_num n2 then res else Lt | a :: n3 => match n2 with | nil => if zerop_num n1 then res else Gt | b :: n4 => let res1 := match a ?= b with | Eq => res | v => v end in cpr_num n3 n4 res1 end end.
imports: List ZArith Znumtheory Uint63 Cyclic63