fact: Fixpoint merge_aux (l1 l2:list A) (b:nat) {struct b} : list A := match b with | O => nil (A:=A) | S b' => match l1, l2 with | nil, l => l | l, nil => l | a :: l, b :: l' => match Ale_dec a b with | left _ => a :: merge_aux l (b :: l') b' | right _ => b :: merge_aux (a :: l) l' b' end end end.
imports: List Lia