proposition: Theorem sort_aux2_permutation : forall (b:nat) (l:list (list A)), length l <= b -> permutation (sort_aux2 l b) (app_all l).
proof: Proof. intros b; elim b; simpl in |- *; auto. - intros l; case l; simpl in |- *; try constructor. intros l' tl H; inversion H. - intros b' Hrec l; case l. + simpl in |- *; intros; constructor. + intros l1 tl; case tl. * simpl in |- *; intros; rewrite app_nil_r; apply permutation_reflexive. * intros l2 tl' Hle; apply permutation_transitive with (app_all (sort_aux1 (l1 :: l2 :: tl'))). apply Hrec. simpl in Hle; generalize (sort_aux1_shorter tl'). simpl in |- *; intros Hle'; lia. apply sort_aux1_permutation. Qed.
imports: List Lia