proposition: Theorem lap_mul_add_distr_l : ∀ la lb lc, lap_eq (lap_mul la (lap_add lb lc)) (lap_add (lap_mul la lb) (lap_mul la lc)).
proof: Proof. intros la lb lc. unfold lap_mul. remember (pred (length la + length (lap_add lb lc))) as labc. remember (pred (length la + length lb)) as lab. remember (pred (length la + length lc)) as lac. rewrite Heqlabc. rewrite lap_convol_mul_more with (n := (lab + lac)%nat). rewrite <- Heqlabc. symmetry. rewrite Heqlab. rewrite lap_convol_mul_more with (n := (labc + lac)%nat). rewrite <- Heqlab. rewrite lap_add_comm. rewrite Heqlac. rewrite lap_convol_mul_more with (n := (labc + lab)%nat). rewrite <- Heqlac. rewrite Nat.add_comm. rewrite lap_add_comm. rewrite Nat.add_assoc, Nat.add_shuffle0, Nat.add_comm, Nat.add_assoc. symmetry. rewrite lap_convol_mul_lap_add. rewrite lap_add_lap_convol_mul. reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation