proposition: Lemma nth_listReplace_ne : forall (i1 i2 : nat)(A : Set)(ls : list A)(a def : A), i1 <> i2 -> nth i1 (listReplace ls i2 a def) def = nth i1 ls def.
proof: Proof. induction i1; destruct i2; destruct ls; intuition; simpl in *. destruct i1; trivial. rewrite IHi1. eapply nth_nil. lia. eapply IHi1. lia. Qed.
imports: FCF.Rat List Permutation Arith FCF.EqDec FCF.StdNat Bool Permutation