proposition: Lemma AbsList_P2 : forall (l:list R) (x y:R), In y (AbsList l x) -> exists z : R, In z l /\ y = Rabs (z - x) / 2.
proof: Proof. intros; induction l as [| r l Hrecl]. - elim H. - elim H; intro. + exists r; split. * simpl; tauto. * symmetry. assumption. + assert (H1 := Hrecl H0); elim H1; intros; elim H2; clear H2; intros; exists x0; simpl; simpl in H2; tauto. Qed.
imports: List Rbase Rfunctions