proposition: Lemma RList_P24 : forall l1 l2:list R, l2 <> nil -> pos_Rl (app l1 l2) (pred (length (app l1 l2))) = pos_Rl l2 (pred (length l2)).
proof: Proof. induction l1 as [ | r r0 H]. - intros; reflexivity. - intros; rewrite <- (H l2 H0); induction l2 as [| r1 l2 Hrecl2]. + elim H0; reflexivity. + do 2 rewrite app_length; replace (length (r :: r0) + length (r1 :: l2))%nat with (S (S (length r0 + length l2))); [ replace (length r0 + length (r1 :: l2))%nat with (S (length r0 + length l2)); [ reflexivity | simpl; apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; rewrite S_INR; ring ] | simpl; apply INR_eq; do 3 rewrite S_INR; do 2 rewrite plus_INR; rewrite S_INR; ring ]. Qed.
imports: List Rbase Rfunctions