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