proposition: Theorem lap_mul_cons_r : ∀ la b lb, lap_eq (lap_mul la [b … lb]) (lap_add (lap_mul la [b]) [0%K … lap_mul la lb]).
proof: Proof. intros la b lb. rewrite lap_mul_comm. rewrite lap_mul_cons_l. rewrite lap_mul_comm. apply lap_add_compat; [ reflexivity | idtac ]. rewrite lap_mul_comm; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation