proposition: Lemma lte_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 !(lte_fin,lee_fin). - by move=> *; rewrite ltr_pM. - move=> x10 x20 xy1 xy2. by rewrite mulry gtr0_sg ?mul1e -?EFinM ?ltry// (le_lt_trans _ xy1). - move=> x10 x20 xy1 xy2. by rewrite mulyr gtr0_sg ?mul1e -?EFinM ?ltry// (le_lt_trans _ xy2). - by move=> *; rewrite mulyy -EFinM ltry. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra) signed