proposition: Lemma Zlt_mult_cancel_l : forall x y z : Z, (0 < x)%Z -> (x * y < x * z)%Z -> (y < z)%Z.
proof: Proof. intros. apply Z.gt_lt. apply Zgt_mult_reg_absorb_l with x. apply Z.lt_gt. assumption. apply Z.lt_gt. assumption. Qed.
imports: Coq(Lia)