proposition: Theorem list_nth_lap_convol_mul_aux : ∀ la lb n i len, pred (List.length la + List.length lb) = (i + len)%nat → (List.nth n (lap_convol_mul r la lb i len) 0%K = Σ (j = 0, n + i), List.nth j la 0 * List.nth (n + i - j) lb 0)%K.
proof: Proof. intros la lb n i len Hlen. revert la lb i n Hlen. induction len; intros. simpl. rewrite Nat.add_0_r in Hlen. rewrite all_0_summation_0; [ destruct n; reflexivity | idtac ]. intros j (_, Hj). destruct (le_dec (length la) j) as [H₁| H₁]. rewrite List.nth_overflow; [ idtac | assumption ]. rewrite rng_mul_0_l; reflexivity. destruct (le_dec (length lb) (n + i - j)) as [H₂| H₂]. rewrite rng_mul_comm. rewrite List.nth_overflow; [ idtac | assumption ]. rewrite rng_mul_0_l; reflexivity. exfalso; apply H₂; clear Hj H₂. apply Nat.nle_gt in H₁; subst i. rewrite <- Nat.add_pred_l. apply Nat.lt_le_pred in H₁. apply Nat.le_add_le_sub_l. rewrite Nat.add_assoc. apply Nat.add_le_mono_r. rewrite Nat.add_comm. 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. simpl. destruct n; [ reflexivity | idtac ]. rewrite Nat.add_succ_r, <- Nat.add_succ_l in Hlen. rewrite IHlen; [ idtac | assumption ]. rewrite Nat.add_succ_r, <- Nat.add_succ_l; reflexivity. Qed.
imports: Utf8 QArith NPeano Misc Field2 Fsummation