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