proposition: Lemma nth_order_replace_neq A: forall n k1 k2, k1 <> k2 -> forall (v : t A n) a (H1 : k1 < n) (H2 : k2 < n), nth_order (replace v (Fin.of_nat_lt H2) a) H1 = nth_order v H1.
proof: Proof. intros n k1 k2 H v a H1 H2. unfold nth_order. rewrite nth_replace_neq; [reflexivity|]. intros E. apply H. apply (f_equal (fun p => proj1_sig (Fin.to_nat p))) in E. now rewrite !Fin.to_nat_of_nat in E. Qed.
imports: VectorDef PeanoNat Eqdep_dec