proposition: Theorem lap_power_add : ∀ la i j, lap_eq (lap_power la (i + j)) (lap_mul (lap_power la i) (lap_power la j)).
proof: Proof. intros la i j. revert j. induction i; intros; simpl. rewrite lap_mul_1_l; reflexivity. rewrite IHi, lap_mul_assoc; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation