fact: Fixpoint T3add x y := if x is cons a b c n d then if y is cons a' b' c' n' d' then if [a,b,c] < [a',b',c'] then y else if [a',b',c'] < [a,b,c] then cons a b c n (d + y) else cons a b c (n+n').+1 d' else x else y where "x + y" := (T3add x y) : ak_scope.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)