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