proposition: Lemma insert_nth_permut': forall (l l': list A) el n, permutation eqA_dec l l' -> permutation eqA_dec (insert_nth l n el) (el::l').
proof: Proof. intros; intro w. unfold insert_nth. change (el :: finalSeg l n) with ((el :: nil) ++ finalSeg l n). change (el :: l') with ((el :: nil) ++ l'). rewrite !list_contents_app. simpl. rewrite Nat.add_0_r. match goal with | |- ?a + (?b + ?c) = ?d => replace (a + (b + c)) with (a + c + b) end. replace (multiplicity (list_contents eqA_dec (initialSeg l n)) w + multiplicity (list_contents eqA_dec (finalSeg l n)) w) with (multiplicity (list_contents eqA_dec (initialSeg l n ++ finalSeg l n)) w). rewrite initialSeg_finalSeg_full; trivial. rewrite (H w); auto with arith. rewrite list_contents_app; trivial. lia. Qed.
imports: Coq(Setoid Morphisms Basics) CoLoR(ListExtras NatUtil LogicUtil)