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