proposition: Lemma list_prod_cons_r A (l : list A) B a (m : list B) : Permutation (list_prod l (a :: m)) (map (fun x => (x,a)) l ++ list_prod l m).
proof: Proof. induction l; ins. eapply Permutation_cons; ins. eapply Permutation_trans; [by apply Permutation_app; eauto|]. rewrite !app_assoc; eauto using Permutation_app, Permutation_app_comm. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation