proposition: Lemma replace_keep_others : forall (l : list A) (i p : nat) (x : A), i < length l -> p < length l -> i <> p -> elemlist A (replace l p x) i = elemlist A l i.
proof: Proof. simple induction l. simpl in |- *. intros. absurd (i < 0). apply lt_n_O. exact H. simple induction i. intros. unfold elemlist in |- *. rewrite elemlist_inv. rewrite elemlist_inv. generalize H1 H2. elim p. intros. absurd (0 <> 0). unfold not in |- *; auto with arith. exact H4. intros. simpl in |- *. rewrite elemlist_cons_O. rewrite elemlist_cons_O. trivial with arith. simple induction p. intros. simpl in |- *. rewrite elemlist_cons_S. rewrite elemlist_cons_S. trivial with arith. intros. clear H1. simpl in |- *. do 2 rewrite elemlist_cons_S. clear H0. apply H. apply lt_S_n. generalize H2; simpl in |- *; trivial with arith. apply lt_S_n. generalize H3; simpl in |- *; trivial with arith. generalize H4. red in |- *. auto with arith. Qed.
imports: Lists_field