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