proposition: Lemma lee_pmul x1 y1 x2 y2 : 0 <= x1 -> 0 <= x2 -> x1 <= y1 -> x2 <= y2 -> x1 * x2 <= y1 * y2.
proof: Proof. move: x1 y1 x2 y2 => [x1| |] [y1| |] [x2| |] [y2| |] //; rewrite !lee_fin. - exact: ler_pM. - rewrite le_eqVlt => /predU1P[<- x20 y10 _|x10 x20 xy1 _]. by rewrite mul0e mule_ge0// leey. by rewrite mulr_infty gtr0_sg// ?mul1e ?leey// (lt_le_trans x10). - rewrite le_eqVlt => /predU1P[<- _ y10 _|x10 _ xy1 _]. by rewrite mul0e mule_ge0// leey. rewrite mulr_infty gtr0_sg// mul1e mulr_infty gtr0_sg// ?mul1e//. exact: (lt_le_trans x10). - move=> x10; rewrite le_eqVlt => /predU1P[<- _ y20|x20 _ xy2]. by rewrite mule0 mulr_infty mule_ge0// ?leey// lee_fin sgr_ge0. by rewrite mulr_infty gtr0_sg ?mul1e ?leey// (lt_le_trans x20). - by move=> x10 x20 _ _; rewrite mulyy leey. - rewrite le_eqVlt => /predU1P[<- _ _ _|x10 _ _ _]. by rewrite mulyy mul0e leey. by rewrite mulyy mulr_infty gtr0_sg// mul1e. - move=> _; rewrite le_eqVlt => /predU1P[<- _ y20|x20 _ xy2]. by rewrite mule0 mulr_infty mule_ge0// ?leey// lee_fin sgr_ge0. rewrite mulr_infty gtr0_sg// mul1e mulr_infty gtr0_sg ?mul1e//. exact: (lt_le_trans x20). - move=> _; rewrite le_eqVlt => /predU1P[<- _ _|x20 _ _]. by rewrite mule0 mulyy leey. by rewrite mulr_infty gtr0_sg// mul1e// mulyy. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed