proposition: Lemma trail : forall dl (e : Qpos) (a b:X), ball (proj1_sig e) a b -> proj1_sig e < Qpos_sum dl -> let n := length dl in (exists2 f : nat -> X, f 0 = a /\ f n = b & forall i z, i < n -> ball (proj1_sig (nth i dl z)) (f i) (f (S i)))%nat.
proof: Proof. induction dl. intros e a b H H1. simpl in *. - exfalso. destruct e. simpl in H1. apply (Qlt_not_le _ _ H1). apply Qlt_le_weak, q. - rename a into x. intros e a b B pe. simpl in pe. destruct dl. simpl in *. pose (f:= (fun n => match n with O => a | S _ => b end)). exists f; auto. intros [|i] z H;[|exfalso; auto with *]. clear z H. ring_simplify in pe. apply ball_weak_le with (proj1_sig e). apply Qlt_le_weak; assumption. assumption. set (Sigma := Qpos_sum (q::dl)). pose (g := ((Qmax 0 (proj1_sig e- proj1_sig x))+Sigma) * (1#2)). assert ((Qmax 0 (proj1_sig e- proj1_sig x))<Sigma). { apply Qmax_case. intros. apply (Qlt_le_trans _ (proj1_sig q)). destruct q; apply q. unfold Sigma. simpl. apply (Qle_trans _ (proj1_sig q+0)). rewrite Qplus_0_r. apply Qle_refl. apply Qplus_le_r. apply Qpos_sum_nonneg. intros. apply (Qplus_lt_l _ _ (proj1_sig x)). ring_simplify. exact pe. } assert (Hg1:=Qsmallest_less_average _ _ H). assert (0<g). refine (Qle_lt_trans _ _ _ _ Hg1). apply Qmax_ub_l. assert (proj1_sig e < proj1_sig x+ g) as H1. { apply (Qplus_lt_l _ _ (-proj1_sig x)). ring_simplify. refine (Qle_lt_trans _ _ _ _ Hg1). apply Qmax_ub_r. } assert (g< Sigma). { apply Qaverage_less_greatest. exact H. } destruct (@prelength a b e x (exist _ _ H0) H1 B) as [c Hc1 Hc2]. destruct (IHdl _ _ _ Hc2 H2) as [f' [Hf'1 Hf'2] Hf'3]. exists (fun n => match n with O => a | S n' => f' n' end). auto. intros [|i] z Hi. simpl. congruence. apply Hf'3. auto with *. Qed.
imports: CoRN.metric2.Metric CoRN.metric2.UniformContinuity CoRN.metric2.Complete CoRN.model.totalorder.QMinMax CoRN.model.totalorder.QposMinMax CoRN.stdlib_omissions.List CoRN.stdlib_omissions.Q