proposition: Theorem exist_first_max : forall l : list nat, l <> [] -> exists a : nat, (exists l1 : list nat, (exists l2 : list nat, l = l1 ++ a :: l2 /\ (forall n1, In n1 l1 -> n1 < a) /\ (forall n1, In n1 l2 -> n1 <= a))).
proof: Proof. intros l; elim l; simpl in |- *; auto. intros H; case H; auto. intros a l0; case l0. intros H H0; exists a; exists []; exists []; repeat (split; simpl in |- *; auto with datatypes). intros n1 H1; case H1. intros n1 H1; case H1. intros n l1 H H0; case H; clear H; auto. red in |- *; intros H1; discriminate; auto. intros a1 (l2, (l3, (HH1, (HH2, HH3)))). case (Nat.le_gt_cases a1 a); intros HH4; auto. exists a; exists []; exists (n :: l1); repeat (split; auto with datatypes). intros n1 H1; case H1. rewrite HH1. intros n1 H1; apply Nat.le_trans with (2 := HH4); case in_app_or with (1 := H1); auto with arith. intros H2; apply Nat.lt_le_incl; auto. simpl in |- *; intros [H2| H2]; [ rewrite H2 | idtac ]; auto. exists a1; exists (a :: l2); exists l3; repeat (split; simpl in |- *; auto with datatypes). apply f_equal2 with (f := cons (A:=nat)); auto. intros n1 [H2| H2]; [ rewrite <- H2 | idtac ]; auto. Qed.
imports: Coq(Inverse_Image Wf_nat Sorting.Permutation)