proposition: Lemma dot_product_id : forall i n (ip : i < n) v, dot_product (id_vec ip) v =A= Vnth v ip.
proof: Proof. induction i. intros. destruct n. lia. VSntac v. unfold id_vec, dot_product. simpl. change (dot_product (Vconst A0 n) (Vtail v) + A1 * Vhead v =A= Vhead v). rewrite dot_product_zero. ring. apply Vforall_nth_intro. intros. rewrite Vnth_const. refl. intros. destruct n. lia. VSntac v. unfold dot_product. simpl. rewrite <- (IHi n (NatCompat.lt_S_n ip) (Vtail v)). ring_simplify. unfold dot_product. refl. Qed.
imports: Coq(Setoid Morphisms) CoLoR(VecUtil RelUtil SemiRing OrdSemiRing NatUtil LogicUtil)