proposition: Lemma RList_P8 : forall (l:list R) (a x:R), In x (insert l a) <-> x = a \/ In x l.
proof: Proof. induction l as [ | r r0 H]. - intros; split; intro; destruct H as [ax | []]; left; symmetry; exact ax. - intros; split; intro. + simpl in H0; generalize H0; case (Rle_dec r a); intros. * simpl in H1; elim H1; intro. -- right; left; assumption. -- elim (H a x); intros; elim (H3 H2); intro. ++ left; assumption. ++ right; right; assumption. * simpl in H1; decompose [or] H1. -- left; symmetry; assumption. -- right; left; assumption. -- right; right; assumption. + simpl; case (Rle_dec r a); intro. * simpl in H0; decompose [or] H0. -- right; elim (H a x); intros; apply H3; left. assumption. -- left. assumption. -- right; elim (H a x); intros; apply H3; right; assumption. * simpl in H0; decompose [or] H0; [ left | right; left | right; right]; trivial; symmetry; assumption. Qed.
imports: List Rbase Rfunctions