proposition: Lemma Zmin_cancel_Zlt : forall x y : Z, (- x < - y)%Z -> (y < x)%Z.
proof: Proof. intros. apply Zgt_mult_conv_absorb_l with (a := (-1)%Z). constructor. replace (-1 * y)%Z with (- y)%Z. replace (-1 * x)%Z with (- x)%Z. apply Z.lt_gt. assumption. ring. ring. Qed.
imports: Coq(Lia)