proposition: Lemma length_replace : forall (l : list A) (p : nat) (x : A), p < length l -> length (replace l p x) = length l.
proof: Proof. simple induction l. simpl in |- *. try trivial with arith. simple induction p. intros. simpl in |- *. apply eq_S. try trivial with arith. intros. clear H0. simpl in |- *. rewrite H. try trivial with arith. auto with arith. Qed.
imports: Lists_field