proposition: Lemma permutation_drop: forall (l l': list A) a b p, eqA a b -> nth_error l' p = Some b -> permutation eqA_dec (a :: l) l' -> permutation eqA_dec l (drop_nth l' p).
proof: Proof. intros; intro el. destruct (eqA_dec a el). assert (eqA el b). apply (Seq_trans A eqA eqA_Equivalence) with a; intuition. rewrite (multiplicity_dropNth_eq eqA_dec eqA_Equivalence l' p el H0 H2). set (w := H1 el); simpl in w. replace (if eqA_dec a el then 1 else 0) with 1 in w. lia. clear w; destruct (eqA_dec a el); [trivial | contr]. assert (~eqA el b). intro elb. absurd (eqA a el); trivial. apply (Seq_trans A eqA eqA_Equivalence) with b; intuition. rewrite (multiplicity_dropNth_neq eqA_dec eqA_Equivalence l' p el H0 H2). set (w := H1 el); simpl in w. replace (if eqA_dec a el then 1 else 0) with 0 in w. lia. clear w; destruct (eqA_dec a el); [contr | trivial]. Qed.
imports: Coq(Setoid Morphisms Basics) CoLoR(ListExtras NatUtil LogicUtil)