proposition: Theorem Zlt_mult_simpl_l : forall a b c : Z, (0 < c)%Z -> (c * a < c * b)%Z -> (a < b)%Z.
proof: Proof. intros a b0 c H H0; apply Z.gt_lt. apply Zmult_gt_reg_r with (p := c); try apply Z.lt_gt; lia. Qed.
imports: Reals ZArith List PeanoNat Psatz