proposition: Theorem sort_aux1_all_sorted : forall l:list (list A), all_sorted l -> all_sorted (sort_aux1 l).
proof: Proof. intros l; elim l using list_ind2. - simpl in |- *; trivial. - simpl in |- *; trivial. - intros x1 x2 tl Hrec Has; inversion Has; clear Has. match goal with | id:(all_sorted _) |- _ => inversion id end. simpl in |- *; constructor. + apply merge_sorted; auto. + auto. Qed.
imports: List Lia