proposition: Lemma list_prod_app A (l l' : list A) B (m : list B) : list_prod (l ++ l') m = list_prod l m ++ list_prod l' m.
proof: Proof. by induction l; ins; rewrite IHl, app_assoc. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation