proposition: Lemma RList_P13 : forall (l:list R) (i:nat) (a:R), (i < pred (length l))%nat -> pos_Rl (mid_Rlist l a) (S i) = (pos_Rl l i + pos_Rl l (S i)) / 2.
proof: Proof. induction l as [ | r r0 H]. - intros; simpl in H; elim (Nat.nlt_0_r _ H). - induction r0 as [ | r1 r2 H0]. + intros; simpl in H0; elim (Nat.nlt_0_r _ H0). + intros; simpl in H1; induction i as [| i Hreci]. * reflexivity. * change (pos_Rl (mid_Rlist (r1 :: r2) r) (S i) = (pos_Rl (r1 :: r2) i + pos_Rl (r1 :: r2) (S i)) / 2). apply H; simpl; apply Nat.succ_lt_mono; assumption. Qed.
imports: List Rbase Rfunctions