fact: Fixpoint sub_num (n1 n2 : number) := match n1 with | nil => nil | a :: n3 => match n2 with | nil => n1 | b :: n4 => let c := a - b in match c ?= a with | Gt => c :: sub1_num n3 n4 | _ => c :: sub_num n3 n4 end end end with sub1_num (n1 n2 : number) := match n1 with | nil => nil | a :: n3 => match n2 with | nil => decr_num n1 | b :: n4 => let c := (a - (1 + b)) in match c ?= a with | Lt => c :: sub_num n3 n4 | _ => c :: sub1_num n3 n4 end end end.
imports: List ZArith Znumtheory Uint63 Cyclic63