proposition: Theorem lap_convol_mul_more : ∀ α (r : ring α) la lb i n, lap_eq (lap_convol_mul r la lb i (pred (length la + length lb))) (lap_convol_mul r la lb i (pred (length la + length lb) + n)).
proof: Proof. intros α r la lb i n. induction n; [ rewrite Nat.add_0_r; reflexivity | idtac ]. rewrite Nat.add_succ_r. rewrite lap_convol_mul_succ. rewrite IHn. apply lap_eq_app_0s. constructor; [ idtac | constructor ]. apply all_0_summation_0. intros j (_, Hj). apply rng_mul_eq_0. destruct (le_dec (length la) j) as [H₁| H₁]. left. rewrite List.nth_overflow; [ reflexivity | assumption ]. apply Nat.nle_gt in H₁. destruct (le_dec (length lb) (i + (pred (length la + length lb) + n) - j)) as [H₂| H₂]. right. rewrite List.nth_overflow; [ reflexivity | assumption ]. exfalso; apply H₂; clear H₂. rewrite <- Nat.add_pred_l. apply Nat.lt_le_pred in H₁. apply Nat.le_add_le_sub_l. rewrite Nat.add_shuffle0, Nat.add_assoc. apply Nat.add_le_mono_r. rewrite Nat.add_comm, <- Nat.add_assoc. eapply Nat.le_trans; eauto . apply Nat.le_sub_le_add_l. rewrite Nat.sub_diag. apply Nat.le_0_l. intros H; rewrite H in H₁. revert H₁; apply Nat.nlt_0_r. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation