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