proposition: Theorem merge_aux_permutation : forall (b:nat) (l1 l2:list A), length l1 + length l2 <= b -> permutation (merge_aux l1 l2 b) (l1 ++ l2).
proof: Proof. intros b; elim b. - intros l1 l2; case l1; case l2; try (simpl in |- *; intros; match goal with | id:(S _ <= _) |- _ => inversion id; fail end). simpl in |- *; constructor. - intros b' Hrec l1 l2; case l1. simpl in |- *; intros Hle; apply permutation_reflexive. + simpl in |- *; intros a l; case l2. simpl in |- *; intros Hle; rewrite app_nil_r; apply permutation_reflexive. simpl in |- *; intros a' l'; case (Ale_dec a a'). * intros Hale Hle; apply permutation_transitive with (a :: a' :: l ++ l'). apply permutation_same_head. apply permutation_transitive with (l ++ a' :: l'). apply (Hrec l (a' :: l')). simpl in |- *; lia. apply permutation_app_cons. constructor. apply permutation_symmetric. apply permutation_app_cons. * intros Hale Hle. apply permutation_transitive with (a' :: a :: l ++ l'). apply permutation_same_head. apply (Hrec (a :: l) l'). simpl in |- *; lia. apply permutation_transitive with (a :: a' :: l ++ l'). constructor. apply permutation_same_head. apply permutation_symmetric. apply permutation_app_cons. Qed.
imports: List Lia