proposition: Lemma nth_dotmuldiv u a b p k : nth (dotmuldiv u a b p) k = if [|| size p <= k, seq.size a <= k | seq.size b <= k] then C.zero else C.mul u (C.div u (C.fromZ u (seq.nth 0%Z a k)) (C.fromZ u (seq.nth 0%Z b k))) (nth p k).
proof: Proof. elim: p a b k => [|c p IHp] a b k; case: a; case: b =>//=; rewrite /nth ?nth_nil //. by rewrite orbT. by rewrite orbT. by move=> *; rewrite leq0n !orbT. by move=> a0 a b0 b; case: k => [|k] //=; rewrite [LHS]IHp ltnS; case: ifP. Qed.
imports: Coq(ZArith Reals) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect ssrfun ssrbool eqtype ssrnat seq fintype bigop) Flocq(Core) Stdlib MathComp Interval Xreal Basic_rec