fact: Fixpoint list_ecompare (l1 l2 : list A) : comparison*flag := match l1, l2 with | [], [] => (Eq,EOL) | [], _ => (Lt,EOL) | _, [] => (Gt,EOL) | x1::l1', x2::l2' => elex (cmp x1 x2) (list_ecompare l1' l2') end.
imports: Coq(List)