proposition: Lemma lt_mult_right : forall x y z : nat, x < y -> 0 < z -> x * z < y * z.
proof: Proof. intros x y z H H0. induction z as [| z Hrecz]. elim (Nat.lt_irrefl _ H0). rewrite Nat.mul_comm. replace (y * S z) with (S z * y); auto with arith. Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid