proposition: Lemma rev_eq_cons A (a : A) (l l' : list A) : rev l = a :: l' <-> l = rev l' ++ a :: nil.
proof: Proof. by rewrite <- rev_eq, rev_rev. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation