proposition: Theorem sort_aux2_sorted : forall (b:nat) (l:list (list A)), length l <= b -> all_sorted l -> sorted (sort_aux2 l b).
proof: Proof. induction b as [ | b IHb]. - intros l; case l. + intros; constructor. + simpl in |- *; intros a l' Hle; inversion Hle. - intro l; case l. + simpl in |- *; intros; constructor. + intros l1 tl; case tl. * intros Hle Has; inversion Has; assumption. * simpl in |- *; intros l2 tl' Hle Has; apply IHb. simpl in |- *. generalize (sort_aux1_shorter tl'); intros; lia. inversion Has; clear Has. match goal with | id:(all_sorted _) |- _ => inversion id end. constructor. apply merge_sorted; assumption. apply sort_aux1_all_sorted; assumption. Qed.
imports: List Lia