proposition: Lemma RList_P3 : forall (l:list R) (x:R), In x l <-> (exists i : nat, x = pos_Rl l i /\ (i < length l)%nat).
proof: Proof. intros; split; intro; [ induction l as [| r l Hrecl] | induction l as [| r l Hrecl] ]. - elim H. - elim H; intro; [ exists 0%nat; split; [ symmetry; apply H0 | simpl; apply Nat.lt_0_succ ] | elim (Hrecl H0); intros; elim H1; clear H1; intros; exists (S x0); split; [ apply H1 | simpl; apply -> Nat.succ_lt_mono; assumption ] ]. - elim H; intros; elim H0; intros; elim (Nat.nlt_0_r _ H2). - simpl; elim H; intros; elim H0; clear H0; intros; induction x0 as [| x0 Hrecx0]; [ left; symmetry; apply H0 | right; apply Hrecl; exists x0; split; [ apply H0 | simpl in H1; apply Nat.succ_lt_mono; assumption ] ]. Qed.
imports: List Rbase Rfunctions