fact: Fixpoint plus (c1 c2 : T1) {struct c1}:T1 := match c1,c2 with | zero, y => y | cons zero n _, zero => cons zero n zero | x, zero => x | cons zero n _, cons zero n' _ => cons zero (S (n+n')) zero | cons a n b, cons a' n' b' => (match compare a a' with | Datatypes.Lt => cons a' n' b' | Gt => (cons a n (plus b (cons a' n' b'))) | Datatypes.Eq => (cons a (S(n+n')) b') end) end where "a + b" := (plus a b) : cantor_scope.
imports: Arith Omega Compare_dec Relations Wellfounded Tools More_nat Wf_nat AccP not_decreasing ArithRing term rpo List