proposition: Lemma Rseq_bound_prod : forall (Un Vn : Rseq) (lu lv : R), Rseq_bound Un lu -> Rseq_bound Vn lv -> Rseq_bound ((Un # Vn) / Rseq_shift INR) (lu * lv).
proof: Proof. intros Un Vn lu lv Un_bd Vn_bd n ; unfold Rseq_prod, Rseq_div ; apply Rseq_bound_sum ; apply Rseq_bound_mult ; [apply Un_bd | intro p ; apply Vn_bd]. Qed.
imports: Lia Rsequence_def Rsequence_base_facts Rsequence_sums_facts Rsequence_rewrite_facts Lra MyRIneq