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