proposition: Theorem lap_compose_single : ∀ a lb lc, (lap_compose ([a] * lb) lc = [a] * lap_compose lb lc)%lap.
proof: Proof. intros a lb lc. induction lb as [| b]. simpl; rewrite lap_mul_nil_r; reflexivity. rewrite lap_mul_cons_r; simpl. rewrite summation_only_one, rng_add_0_r, IHlb. rewrite lap_mul_add_distr_l, lap_mul_assoc. apply lap_add_compat; [ reflexivity | idtac ]. 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