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