proposition: Lemma Zlt_conv_mult_l : forall x y z : Z, (x < 0)%Z -> (y < z)%Z -> (x * y > x * z)%Z.
proof: Proof. intros x y z H H0. cut (- x > 0)%Z. intro H1. cut (- x * y < - x * z)%Z. intro H2. cut (- (- x * y) > - (- x * z))%Z. intro H3. cut (- - (x * y) > - - (x * z))%Z. intro H4. cut ((- - (x * y))%Z = (x * y)%Z). intro H5. rewrite H5 in H4. cut ((- - (x * z))%Z = (x * z)%Z). intro H6. rewrite H6 in H4. assumption. exact (Z.opp_involutive (x * z)). exact (Z.opp_involutive (x * y)). cut ((- (- x * y))%Z = (- - (x * y))%Z). intro H4. rewrite H4 in H3. cut ((- (- x * z))%Z = (- - (x * z))%Z). intro H5. rewrite H5 in H3. assumption. cut ((- x * z)%Z = (- (x * z))%Z). intro H5. exact (f_equal Z.opp H5). exact (Zopp_mult_distr_l_reverse x z). cut ((- x * y)%Z = (- (x * y))%Z). intro H4. exact (f_equal Z.opp H4). exact (Zopp_mult_distr_l_reverse x y). exact (Zlt_opp (- x * y) (- x * z) H2). exact (Zlt_reg_mult_l (- x) y z H1 H0). exact (Zlt_opp x 0 H). Qed.
imports: Coq(Lia) CoRN.stdlib_omissions.List Coq.Logic.Eqdep_dec Coq.Setoids.Setoid