proposition: Lemma permutation_length: forall (l l': list A), permutation eqA_dec l l' -> length l = length l'.
proof: Proof. induction l; intros. simpl. destruct l'; trivial. unfold permutation in H. exfalso. assert (w := H a); simpl in w; clear H. destruct (eqA_dec a a). lia. intuition. destruct (permutation_cons H) as [p [a' [l'p [aa' ll'p]]]]. simpl. rewrite (IHl (drop_nth l' p)); trivial. set (w := nth_some l' p l'p). rewrite drop_nth_in_length; trivial. lia. Qed.
imports: Coq(Setoid Morphisms Basics) CoLoR(ListExtras NatUtil LogicUtil)