proposition: Lemma replace_sym : forall (l : list A) (p p' : nat) (x x' : A), p < length l -> p' < length l -> p <> p' -> replace (replace l p' x') p x = replace (replace l p x) p' x'.
proof: Proof. simple induction l. simpl in |- *. trivial with arith. simple induction p. intros. generalize H1 H2. elim p'. intros. absurd (0 <> 0); unfold not in |- *; auto with arith. intros. simpl in |- *. trivial with arith. simple induction p'. intros. simpl in |- *. trivial with arith. intros. clear H1. clear H0. simpl in |- *. rewrite H. trivial with arith. auto with arith. auto with arith. red in |- *. auto with arith. Qed.
imports: Lists_field