proposition: Theorem Qpositive_plus_le : forall w w' : Qpositive, Qpositive_le w (Qpositive_plus w w').
proof: Proof. intros w w'; apply Qpositive_le'_to_Qpositive_le. unfold Qpositive_le' in |- *. unfold Qpositive_plus in |- *. elim (interp_non_zero w); intros p (q, Heq); elim (interp_non_zero w'); intros p' (q', Heq'). rewrite Heq; rewrite Heq'. expand (S p * S q' + S p' * S q) (S q * S q') (S p * S q' + S p' * S q + S q * S q') ipattern:(d) ipattern:(p'') ipattern:(q'') ipattern:(Heq2) ipattern:(Heq3) ipattern:(Heq4). apply Nat.mul_le_mono_pos_l with (S d); auto with arith. rewrite (Nat.mul_assoc (S d) (S p'')); repeat rewrite (Nat.mul_comm (S d)); rewrite <- (Nat.mul_assoc (S p)); rewrite <- Heq3; rewrite <- Heq4. rewrite Nat.mul_add_distr_r. replace (S p * S q' * S q) with (S p * (S q * S q')). auto with arith. ring. Qed.