proposition: Theorem lap_mul_add_distr_r : ∀ la lb lc, lap_eq (lap_mul (lap_add la lb) lc) (lap_add (lap_mul la lc) (lap_mul lb lc)).
proof: Proof. intros la lb lc. rewrite lap_mul_comm, lap_mul_add_distr_l, lap_mul_comm. apply lap_add_compat; [ reflexivity | apply lap_mul_comm ]. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation