proposition: Lemma CPermutation_length_2_inv : forall a b l, CPermutation [a; b] l -> l = [a; b] \/ l = [b; a].
proof: Proof. intros; now apply Permutation_length_2_inv, CPermutation_Permutation. Qed.
imports: List Permutation Morphisms PeanoNat