proposition: Lemma cvgeM f g (a b : \bar R) : a *? b -> f @ F --> a -> g @ F --> b -> f \* g @ F --> a * b.
proof: Proof. move=> [:apoo] [:bnoo] [:poopoo] [:poonoo]; move: a b => [a| |] [b| |] //. - move=> _ /fine_cvgP[finf fa] /fine_cvgP[fing gb]. apply/fine_cvgP; split. by near do apply: fin_numM; [apply: finf | apply: fing]. apply: (@cvg_trans _ (((fine \o f) \* (fine \o g)) @ F)%R). apply: near_eq_cvg; near=> n => //=. rewrite -[in RHS](@fineK _ (f n)); last by near: n; exact: finf. by rewrite -[in RHS](@fineK _ (g n)) //; near: n; exact: fing. exact: cvgM. - move: f g a; abstract: apoo. move=> {}f {}g {}a + fa goo; have [a0 _|a0 _|->] := ltgtP a 0%R. + rewrite mulry ltr0_sg// ?mulN1e. by under eq_fun do rewrite muleC; exact: (cvgeM_lt0_pinfty a0). + rewrite mulry gtr0_sg// ?mul1e. by under eq_fun do rewrite muleC; exact: (cvgeM_gt0_pinfty a0). + by rewrite /mule_def eqxx. - move: f g a; abstract: bnoo. move=> {}f {}g {}a + fa goo; have [a0 _|a0 _|->] := ltgtP a 0%R. + rewrite mulrNy ltr0_sg// ?mulN1e. by under eq_fun do rewrite muleC; exact: (cvgeM_lt0_ninfty a0). + rewrite mulrNy gtr0_sg// ?mul1e. by under eq_fun do rewrite muleC; exact: (cvgeM_gt0_ninfty a0). + by rewrite /mule_def eqxx. - rewrite mule_defC => ? foo gb; rewrite muleC. by under eq_fun do rewrite muleC; exact: apoo. - move=> _; move: f g; abstract: poopoo. move=> {}f {}g /cvgeyPge foo /cvgeyPge goo. rewrite mulyy; apply/cvgeyPgey; near=> A; near=> n. have A_gt0 : (0 <= A)%R by []. by rewrite -[leLHS]mule1 lee_pmul//=; near: n; [apply: foo|apply: goo]. - move=> _; move: f g; abstract: poonoo. move=> {}f {}g /cvgeyPge foo /cvgeNyPle goo. rewrite mulyNy; apply/cvgeNyPle => A; near=> n. rewrite (@le_trans _ _ (g n))//; last by near: n; exact: goo. apply: lee_nemull; last by near: n; apply: foo. by rewrite (@le_trans _ _ (- 1)%:E)//; near: n; apply: goo; rewrite ltrN10. - rewrite mule_defC => ? foo gb; rewrite muleC. by under eq_fun do rewrite muleC; exact: bnoo. - move=> _ foo goo. by under eq_fun do rewrite muleC; exact: poonoo. - move=> _ foo goo; rewrite mulNyNy -mulyy. by under eq_fun do rewrite -muleNN; apply: poopoo; rewrite -/(- -oo); apply: cvgeN. Unshelve. all: end_near. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrint ssrnum finmap matrix) mathcomp(rat interval zmodp vector fieldext falgebra) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality set_interval Rstruct) ereal reals signed topology prodnormedzmodule