proposition: Lemma rev_eq_snoc A (a : A) (l l' : list A) : rev l = l' ++ a :: nil <-> l = a :: rev l'.
proof: Proof. apply rev_eq_app. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation