proposition: Lemma RList_P10 : forall (l:list R) (a:R), length (insert l a) = S (length l).
proof: Proof. intros; induction l as [| r l Hrecl]; [ reflexivity | simpl; case (Rle_dec r a); intro; [ simpl; rewrite Hrecl; reflexivity | reflexivity ] ]. Qed.
imports: List Rbase Rfunctions