proposition: Lemma RList_P0 : forall (l:list R) (a:R), pos_Rl (insert l a) 0 = a \/ pos_Rl (insert l a) 0 = pos_Rl l 0.
proof: Proof. intros; induction l as [| r l Hrecl]; [ left; reflexivity | simpl; case (Rle_dec r a); intro; [ right; reflexivity | left; reflexivity ] ]. Qed.
imports: List Rbase Rfunctions