proposition: Lemma app_comm_cons' A (a : A) l l' : l ++ a :: l' = (l ++ a :: nil) ++ l'.
proof: Proof. by rewrite <- app_assoc. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation