proposition: Lemma S2_decrease : forall n u l l', S2 n u l l' -> exists a:T1, ltM a (h2ol l') (h2ol l).
proof: Proof. induction 1. simpl. generalize (R1_decrease _ _ _ r). exists (h2o h). induction n. simpl. apply ltM_head. auto with arith. auto. simpl. apply lt_ltM. auto. auto. exists (h2o h). induction n. simpl. apply ltM_head. auto with arith. eapply R1_decrease. eauto. simpl. simpl in IHn. apply lt_ltM. eapply R1_decrease. eauto. auto. case IHS2; intros. exists x. simpl. apply ltM_cons. auto. Qed.
imports: Arith Omega List EPSILON0 MSE0