proposition: Theorem lap_compose_mul : ∀ la lb lc, (lap_compose (la * lb) lc = lap_compose la lc * lap_compose lb lc)%lap.
proof: Proof. intros la lb lc. revert lb lc. induction la as [| a]; intros; simpl. do 2 rewrite lap_mul_nil_l; reflexivity. destruct lb as [| b]; simpl. do 2 rewrite lap_mul_nil_r; reflexivity. rewrite lap_mul_cons; simpl. do 2 rewrite lap_compose_add; simpl. do 2 rewrite IHla; simpl. rewrite lap_mul_nil_l, lap_add_nil_l. do 3 rewrite lap_mul_add_distr_r; simpl. rewrite lap_mul_add_distr_l; simpl. rewrite lap_mul_add_distr_r; simpl. rewrite lap_mul_add_distr_r; simpl. do 2 rewrite lap_mul_assoc. do 2 rewrite lap_add_assoc; simpl. apply lap_add_compat. rewrite lap_eq_0, lap_mul_nil_l, lap_add_nil_r. rewrite lap_add_comm, lap_add_assoc. rewrite <- lap_add_assoc. rewrite <- lap_add_assoc. apply lap_add_compat. apply lap_mul_compat; [ idtac | reflexivity ]. rewrite lap_mul_shuffle0; reflexivity. symmetry; rewrite lap_add_comm. apply lap_add_compat. rewrite lap_mul_shuffle0; reflexivity. apply lap_mul_compat; [ idtac | reflexivity ]. symmetry. apply lap_compose_single. rewrite lap_mul_cons; simpl. rewrite lap_mul_nil_r. constructor; [ reflexivity | idtac ]. rewrite lap_eq_0; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation