proposition: Lemma Permutation_length_2 : forall a1 a2 b1 b2, Permutation [a1;a2] [b1;b2] -> a1 = b1 /\ a2 = b2 \/ a1 = b2 /\ a2 = b1.
proof: Proof. intros a1 b1 a2 b2 H. apply Permutation_length_2_inv in H as [H|H]; injection H as [= -> ->]; auto. Qed.
imports: List Setoid Compare_dec Morphisms FinFun PeanoNat