fact: Fixpoint T1lt x y {struct x} := if x is cons a n b then if y is cons a' n' b' then if a < a' then true else if a == a' then if (n < n')%N then true else if (n == n') then b < b' else false else false else false else if y is cons a' n' b' then true else false where "x < y" := (T1lt x y) : cantor_scope.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)