proposition: Theorem Qpositive_le_mult : forall w w' w'' : Qpositive, Qpositive_le w w' -> Qpositive_le (Qpositive_mult w w'') (Qpositive_mult w' w'').
proof: Proof. intros w w' w''; make_fraction w ipattern:(p) ipattern:(q) ipattern:(Heq); make_fraction w' ipattern:(p') ipattern:(q') ipattern:(Heq'); make_fraction w'' ipattern:(p'') ipattern:(q'') ipattern:(Heq''). intros H; apply Qpositive_le'_to_Qpositive_le; generalize (Qpositive_le_to_Qpositive_le' _ _ H); clear H. unfold Qpositive_le', Qpositive_mult in |- *; simpl in |- *; rewrite Heq; rewrite Heq'; rewrite Heq''. expand (S p * S p'') (S q * S q'') (S p * S p'' + S q * S q'') ipattern:(d) ipattern:(p3) ipattern:(q3) ipattern:(Heq3) ipattern:(Heq1) ipattern:(Heq2). expand (S p' * S p'') (S q' * S q'') (S p' * S p'' + S q' * S q'') ipattern:(d') ipattern:(p4) ipattern:(q4) ipattern:(Heq4) ipattern:(Heq5) ipattern:(Heq6). intros Hle; apply Nat.mul_le_mono_pos_l with (S d); auto with arith; rewrite (Nat.mul_comm (S p3)); repeat rewrite (Nat.mul_comm (S d)); repeat rewrite <- Nat.mul_assoc. rewrite <- Heq1; rewrite <- Heq2. apply Nat.mul_le_mono_pos_l with (S d'); auto with arith; repeat rewrite Nat.mul_assoc; repeat rewrite (Nat.mul_comm (S d')); rewrite <- Heq5; rewrite <- Heq6. replace (S q' * S q'' * S p * S p'') with (S q'' * S p'' * (S p * S q')). replace (S p' * S p'' * S q * S q'') with (S q'' * S p'' * (S p' * S q)). apply (fun m n p : nat => Nat.mul_le_mono_l p n m); exact Hle. ring. ring. Qed.