proposition: Lemma Permutation_length_2_inv : forall a1 a2 l, Permutation [a1;a2] l -> l = [a1;a2] \/ l = [a2;a1].
proof: Proof. intros a1 a2 l H; remember [a1;a2] as m in H. revert a1 a2 Heqm. induction H; intros; try (injection Heqm as [= ? ?]; subst); discriminate || (try tauto). - apply Permutation_length_1_inv in H as ->; left; auto. - apply IHPermutation1 in Heqm as [H1|H1]; apply IHPermutation2 in H1 as []; auto. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat