proposition: Lemma Rlist_P1 : forall (l:list R) (P:R -> R -> Prop), (forall x:R, In x l -> exists y : R, P x y) -> exists l' : list R, length l = length l' /\ (forall i:nat, (i < length l)%nat -> P (pos_Rl l i) (pos_Rl l' i)).
proof: Proof. intros; induction l as [| r l Hrecl]. - exists nil; intros; split; [ reflexivity | intros; simpl in H0; elim (Nat.nlt_0_r _ H0) ]. - assert (H0 : In r (r :: l)). + simpl; left; reflexivity. + assert (H1 := H _ H0); assert (H2 : forall x:R, In x l -> exists y : R, P x y). * intros; apply H; simpl; right; assumption. * assert (H3 := Hrecl H2); elim H1; intros; elim H3; intros; exists (x :: x0); intros; elim H5; clear H5; intros; split. -- simpl; rewrite H5; reflexivity. -- intros; destruct (zerop i) as [->|]. ++ simpl; assumption. ++ assert (H9 : i = S (pred i)). ** symmetry; apply Nat.lt_succ_pred with 0%nat; assumption. ** rewrite H9; simpl; apply H6; simpl in H7; apply Nat.succ_lt_mono; rewrite <- H9; assumption. Qed.
imports: List Rbase Rfunctions