proposition: Lemma RList_P20 : forall l:list R, (2 <= length l)%nat -> exists r : R, (exists r1 : R, (exists l' : list R, l = r :: r1 :: l')).
proof: Proof. intros; induction l as [| r l Hrecl]; [ simpl in H; elim (Nat.nle_succ_0 _ H) | induction l as [| r0 l Hrecl0]; [ simpl in H; elim (Nat.nle_succ_0 _ (le_S_n _ _ H)) | exists r; exists r0; exists l; reflexivity ] ]. Qed.
imports: List Rbase Rfunctions