proposition: Lemma RList_P19 : forall l:list R, l <> nil -> exists r : R, (exists r0 : list R, l = r :: r0).
proof: Proof. intros; induction l as [| r l Hrecl]; [ elim H; reflexivity | exists r; exists l; reflexivity ]. Qed.
imports: List Rbase Rfunctions