proposition: Lemma led_mul a b c d : a <= c -> b <= d -> a * b <= c * d.
proof: Proof. move=> ac bd; exact/(le_trans (led_mul2r _ ac))/led_mul2l. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype choice order) mathcomp(ssrnat bigop ssralg)