proposition: Lemma Zlt_reg_mult_l : forall x y z : Z, (x > 0)%Z -> (y < z)%Z -> (x * y < x * z)%Z.
proof: Proof. intros. case (Zcompare_Gt_spec x 0). unfold Z.gt in H. assumption. intros. cut (x = Zpos x0). intro. rewrite H2. unfold Z.lt in H0. unfold Z.lt in |- *. cut ((Zpos x0 * y ?= Zpos x0 * z)%Z = (y ?= z)%Z). intro. exact (trans_eq H3 H0). apply Zcompare_mult_compat. cut (x = (x + - (0))%Z). intro. exact (trans_eq H2 H1). simpl in |- *. apply (sym_eq (A:=Z)). exact (Zplus_0_r x). Qed.
imports: Coq(Lia)