proposition: Lemma app_nth A n l l' (d : A) : nth n (l ++ l') d = if le_lt_dec (length l) n then nth (n - length l) l' d else nth n l d.
proof: Proof. desf; eauto using app_nth1, app_nth2. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation