proposition: Lemma Zle_mult_l : forall p q r : Z, (0 < r)%Z -> (p <= q)%Z -> (r * p <= r * q)%Z.
proof: Proof. simple induction r. intros. simpl in |- *. apply Zeq_le. reflexivity. intros. unfold Z.le in |- *. rewrite (Zcompare_mult_compat p0 p q). assumption. intros. unfold Z.lt in H. simpl in H. discriminate H. Qed.
imports: ZArith EqNat