proposition: Lemma RList_P15 : forall l1 l2:list R, ordered_Rlist l1 -> ordered_Rlist l2 -> pos_Rl l1 0 = pos_Rl l2 0 -> pos_Rl (cons_ORlist l1 l2) 0 = pos_Rl l1 0.
proof: Proof. intros; apply Rle_antisym. - induction l1 as [| r l1 Hrecl1]; [ simpl; simpl in H1; right; symmetry ; assumption | elim (RList_P9 (r :: l1) l2 (pos_Rl (r :: l1) 0)); intros; assert (H4 : In (pos_Rl (r :: l1) 0) (r :: l1) \/ In (pos_Rl (r :: l1) 0) l2); [ left; left; reflexivity | assert (H5 := H3 H4); apply RList_P5; [ apply RList_P2; assumption | assumption ] ] ]. - induction l1 as [| r l1 Hrecl1]; [ simpl; simpl in H1; right; assumption | assert (H2 : In (pos_Rl (cons_ORlist (r :: l1) l2) 0) (cons_ORlist (r :: l1) l2)); [ elim (RList_P3 (cons_ORlist (r :: l1) l2) (pos_Rl (cons_ORlist (r :: l1) l2) 0)); intros; apply H3; exists 0%nat; split; [ reflexivity | rewrite RList_P11; simpl; apply Nat.lt_0_succ ] | elim (RList_P9 (r :: l1) l2 (pos_Rl (cons_ORlist (r :: l1) l2) 0)); intros; assert (H5 := H3 H2); elim H5; intro; [ apply RList_P5; assumption | rewrite H1; apply RList_P5; assumption ] ] ]. Qed.
imports: List Rbase Rfunctions