proposition: Lemma countIn_dropNth_eq : forall l p el el', nth_error l p = Some el' -> eqA el el' -> countIn el (drop_nth l p) = countIn el l - 1.
proof: Proof. induction l; intros. destruct p; trivial. destruct p. simpl; rewrite drop_nth_cons; destruct (eqA_dec el a). lia. absurd (eqA el el'); trivial. inversion H; rewrite <- H2; trivial. rewrite drop_nth_succ. simpl; rewrite IHl with p el el'; trivial. destruct (eqA_dec el a); trivial. set (el'l := nth_some_in l p H). assert (el'el: eqA el' el). intuition. set (w := in_countIn l el'l el'el). lia. Qed.
imports: Coq(Permutation Setoid) CoLoR(NatUtil LogicUtil)