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