proposition: Lemma pmul2w1 (a b c d : R) : 0 <= a -> 0 <= d -> a <= b -> c <= d -> a * c <= b * d.
proof: Proof. move => a0 d0 ab cd. apply: (le_trans (ler_wpmul2l a0 cd)). by apply: (le_trans (ler_wpmul2r d0 ab)). Qed.
imports: mathcomp(all_ssreflect) mathcomp(ssralg poly ssrnum ssrint rat polyrcf) mathcomp(polyorder polydiv)