proposition: Theorem lap_power_mul : ∀ la lb n, lap_eq (lap_power (lap_mul la lb) n) (lap_mul (lap_power la n) (lap_power lb n)).
proof: Proof. intros la lb n. revert la lb. induction n; intros; simpl. rewrite lap_mul_1_l; reflexivity. rewrite IHn. do 2 rewrite <- lap_mul_assoc. apply lap_mul_compat; [ reflexivity | idtac ]. do 2 rewrite lap_mul_assoc. apply lap_mul_compat; [ idtac | reflexivity ]. apply lap_mul_comm. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation