fact: Definition phi a b := if b is cons u v n k then if ((n==0) && (k==zero)) then if (a < u) then b else [a,b] else if ((n==0) && (T2finite1 k) && (a <u)) then [a, cons u v 0 (T2pred k) ] else [a,b] else [a,b].
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)