proposition: Lemma le_mult_right : forall x y z : nat, x <= y -> x * z <= y * z.
proof: Proof. intros x y z H. rewrite Nat.mul_comm. rewrite (Nat.mul_comm y). auto with arith. Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid