proposition: Theorem lap_compose_compose2 : ∀ la lb, lap_eq (lap_compose la lb) (lap_compose2 la lb).
proof: Proof. intros la lb. revert lb. induction la as [| a]; intros; [ reflexivity | simpl ]. rewrite IHla. symmetry; clear. unfold lap_compose2. rewrite lap_mul_comm. rewrite lap_mul_fold_add_distr. rewrite lap_add_comm. remember [a] as aa; simpl; subst aa. rewrite lap_add_comm. apply lap_add_compat; [ apply lap_mul_1_r | idtac ]. apply list_fold_right_seq. rewrite lap_mul_nil_r; reflexivity. intros x y z Hyz. rewrite Hyz; reflexivity. intros i accu; simpl. apply lap_add_compat; [ reflexivity | simpl ]. rewrite lap_mul_comm, <- lap_mul_assoc. apply lap_mul_compat; [ reflexivity | idtac ]. apply lap_mul_comm. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation