proposition: Lemma RList_P9 : forall (l1 l2:list R) (x:R), In x (cons_ORlist l1 l2) <-> In x l1 \/ In x l2.
proof: Proof. induction l1 as [ | r r0 H]. - intros; split; intro; [ simpl in H; right; assumption | simpl; elim H; intro; [ elim H0 | assumption ] ]. - intros; split. + simpl; intros; elim (H (insert l2 r) x); intros; assert (H3 := H1 H0); elim H3; intro. * left; right; assumption. * elim (RList_P8 l2 r x); intros H5 _; assert (H6 := H5 H4); elim H6; intro. -- left; left; symmetry; assumption. -- right; assumption. + intro; simpl; elim (H (insert l2 r) x); intros _ H1; apply H1; elim H0; intro. * elim H2; intro. -- right; elim (RList_P8 l2 r x); intros _ H4; apply H4; left. symmetry; assumption. -- left; assumption. * right; elim (RList_P8 l2 r x); intros _ H3; apply H3; right; assumption. Qed.
imports: List Rbase Rfunctions