proposition: Theorem Zle_Zmult_comp_r : forall x y z : Z, (0 <= z)%Z -> (x <= y)%Z -> (x * z <= y * z)%Z.
proof: Proof. intros x y z H' H'0; case (Zle_lt_or_eq _ _ H'); intros Zlt1. apply Zmult_gt_0_le_compat_r; auto. apply Z.lt_gt; auto. rewrite <- Zlt1; repeat rewrite <- Zmult_0_r_reverse; auto with zarith. Qed.
imports: Reals ZArith List PeanoNat Psatz