proposition: Lemma ltr_pmul_le_l R (x1 y1 x2 y2 : R) : 0 < x1 -> 0 < x2 -> x1 <= y1 -> x2 < y2 -> x1 * x2 < y1 * y2.
proof: Proof. rewrite le_eqVlt => posx1 posx2 /predU1P[<-|lt1] lt2. by rewrite ltr_pM2l. by apply: ltr_pM=> //; exact: ltW. Qed.
imports: mathcomp(all_ssreflect all_algebra all_field) mathcomp(bigenough)