proposition: Lemma list_prod_app_r A (l : list A) B (m m' : list B) : Permutation (list_prod l (m ++ m')) (list_prod l m ++ list_prod l m').
proof: Proof. induction m; ins; ins. by rewrite list_prod_nil_r. rewrite list_prod_cons_r. eapply Permutation_trans; [by eapply Permutation_app, IHm|]. rewrite app_assoc; apply Permutation_app; ins. symmetry; apply list_prod_cons_r. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation