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