proposition: Theorem Qgt_mult : forall x y z : Q, Qgt z Zero -> Qgt x y -> Qgt (Qmult z x) (Qmult z y).
proof: Proof. intros x y z; case z. intros H; inversion H. case y; case x; auto. simpl in |- *; auto. intros x' y' H H1; inversion H1. intros x' y' H H1; inversion H1. simpl in |- *; intros x' y' z' H H0; apply Qgt_pos_pos. red in |- *; intros H1. inversion H0. elim H4; rewrite <- (Qpositive_mult_One x'). rewrite <- (Qpositive_mult_One y'). rewrite <- (Qpositive_mult_inv z'). repeat rewrite Qpositive_mult_assoc. repeat rewrite (Qpositive_mult_sym (Qpositive_inv z')). repeat rewrite <- Qpositive_mult_assoc. apply Qpositive_le_mult. auto. intros x' y' z' H H1; inversion H1. simpl in |- *; auto. simpl in |- *; auto. simpl in |- *; intros x' y' z' H H1; apply Qgt_neg_neg. red in |- *; intros H0; inversion H1. elim H4; rewrite <- (Qpositive_mult_One y'). rewrite <- (Qpositive_mult_One x'). rewrite <- (Qpositive_mult_inv z'). repeat rewrite Qpositive_mult_assoc. repeat rewrite (Qpositive_mult_sym (Qpositive_inv z')). repeat rewrite <- Qpositive_mult_assoc. apply Qpositive_le_mult. auto. intros z' H; inversion H. Qed.