fact: Definition getMin := (fix aux1 (l1 l2 : list A) {struct l1} : option A := match l1, l2 with | a :: t1, b :: t2 => match ltADec a b with | inleft (left _) => aux1 t1 (b :: t2) | inleft (right _) => (fix aux2 (l3 : list A) : option A := match l3 with | c :: t3 => match ltADec a c with | inleft (left _) => aux1 t1 (c :: t3) | inleft (right _) => aux2 t3 | inright H => match testDec a c H with | left _ => Some a | right __ => aux2 t3 end end | nil => None end) (b :: t2) | inright H => match testDec a b H with | left _ => Some a | right _ => aux1 t1 t2 end end | nil, _ => None | _, nil => None end).
imports: Coq(Arith) Coq(Lexicographic_Exponentiation)