proposition: Lemma RList_P29 : forall (l2 l1:list R) (i:nat), (length l1 <= i)%nat -> (i < length (app l1 l2))%nat -> pos_Rl (app l1 l2) i = pos_Rl l2 (i - length l1).
proof: Proof. induction l2 as [ | r r0 H]. - intros; rewrite app_nil_r in H0; elim (Nat.lt_irrefl _ (Nat.le_lt_trans _ _ _ H H0)). - intros; replace (app l1 (r :: r0)) with (app (app l1 (r :: nil)) r0). + inversion H0. * rewrite Nat.sub_diag; simpl; rewrite RList_P26. -- clear r0 H i H0 H1 H2; induction l1 as [| r0 l1 Hrecl1]. ++ reflexivity. ++ simpl; assumption. -- rewrite app_length; rewrite Nat.add_comm; simpl; apply Nat.lt_succ_diag_r. * replace (S m - length l1)%nat with (S (S m - S (length l1))). -- rewrite H3; simpl; replace (S (length l1)) with (length (app l1 (r :: nil))). ++ apply (H (app l1 (r :: nil)) i). ** rewrite app_length; rewrite Nat.add_comm; simpl; rewrite <- H3; apply le_n_S; assumption. ** repeat rewrite app_length; simpl; rewrite app_length in H1; rewrite Nat.add_comm in H1; simpl in H1; rewrite (Nat.add_comm (length l1)); simpl; rewrite Nat.add_comm; apply H1. ++ rewrite app_length; rewrite Nat.add_comm; reflexivity. -- change (S (m - length l1) = (S m - length l1)%nat); symmetry; apply Nat.sub_succ_l; assumption. + replace (r :: r0) with (app (r :: nil) r0); [ symmetry ; apply app_assoc | reflexivity ]. Qed.
imports: List Rbase Rfunctions