fact: Definition lt_rec f x y := if x is cons a b n c then if y is cons a' b' n' c' then if ( ((f a a') && (f b ([a', b']))) || ((a == a') && (f b b')) || ((f a' a) && (f ([a, b]) b')) || (((f a' a) && ([a, b] == b')))) then true else if ((a== a') && (b==b')) then if (n < n')%N then true else if (n == n') then (f c c') else false else false else false else if y is cons a' b' n' c' then true else false.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)