proposition: Theorem merge_aux_sorted : forall (b:nat) (l1 l2:list A), length l1 + length l2 <= b -> sorted l1 -> sorted l2 -> sorted (merge_aux l1 l2 b) /\ first_elem_prop l1 l2 (merge_aux l1 l2 b).
proof: Proof. intros b; elim b. - intros l1 l2. case l1; case l2; simpl in |- *; try (intros; match goal with | id:(S _ <= _) |- _ => inversion id; fail end). repeat constructor. - intros b' Hrec l1; case l1. simpl in |- *; intros; split; [ assumption | case l2; constructor ]. intros a l l2; case l2. + simpl in |- *; intros; split; [ assumption | constructor ]. + simpl in |- *; intros a' l' Hle Hsorted1 Hsorted2; case (Ale_dec a a'). * elim (Hrec l (a' :: l')); auto. intros Hsorted' Hfep. generalize Hsorted' Hsorted1 Hsorted2; clear Hsorted1 Hsorted2 Hsorted'. inversion Hfep. intros Hsorted' Hsorted1 Hsorted2 Hale. inversion Hsorted1; repeat constructor || assumption. intros Hsorted' Hsorted1 Hsorted2 Hale. inversion Hsorted2; repeat constructor || assumption. simpl in |- *; lia. eapply sorted_inv; eauto. * elim (Hrec (a :: l) l'); auto. intros Hsorted' Hfep. generalize Hsorted' Hsorted1 Hsorted2; clear Hsorted1 Hsorted2 Hsorted'. inversion Hfep. intros Hsorted' Hsorted1 Hsorted2 Hale. inversion Hsorted1; repeat constructor || assumption. intros Hsorted' Hsorted1 Hsorted2 Hale. inversion Hsorted2; repeat constructor || assumption. simpl in |- *; lia. eapply sorted_inv; eauto. Qed.
imports: List Lia