proposition: Lemma pos_Rl_P1 : forall (l:list R) (a:R), (0 < length l)%nat -> pos_Rl (a :: l) (length l) = pos_Rl l (pred (length l)).
proof: Proof. intros; induction l as [| r l Hrecl]; [ elim (Nat.nlt_0_r _ H) | simpl; case (length l); [ reflexivity | intro; reflexivity ] ]. Qed.
imports: List Rbase Rfunctions