proposition: Lemma permut_conv_inv : forall e l1 l2, permutation (e :: l1) (e :: l2) -> permutation l1 l2.
proof: Proof. intros e l1 l2; unfold permutation, meq; simpl; intros H a; generalize (H a); lia. Qed.
imports: Lia Relations Multiset SetoidList