proposition: Lemma Permutation_listprod_r A (l : list A) B (m m' : list B) : Permutation m m' -> Permutation (list_prod l m) (list_prod l m').
proof: Proof. ins; revert l; induction H; ins; eauto using Permutation. by rewrite ?list_prod_cons_r; eauto using Permutation_app. rewrite list_prod_cons_r. eapply Permutation_trans; [by apply Permutation_app, list_prod_cons_r|]. symmetry. rewrite list_prod_cons_r. eapply Permutation_trans; [by apply Permutation_app, list_prod_cons_r|]. rewrite !app_assoc; eauto using Permutation_app, Permutation_app_comm. Qed.
imports: HahnBase HahnSets Arith Lia Setoid Morphisms Sorted IndefiniteDescription List Permutation