proposition: Theorem Qpositive_le_sub_l : forall w w' w'' : Qpositive, w <> w'' -> w' <> w'' -> Qpositive_le w w'' -> Qpositive_le w' w'' -> Qpositive_le w w' -> Qpositive_le (Qpositive_sub w'' w') (Qpositive_sub 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 Hneq1 Hneq2. intros H H1 H2; apply Qpositive_le'_to_Qpositive_le; generalize (Qpositive_le_to_Qpositive_le' _ _ H) (Qpositive_le_to_Qpositive_le' _ _ H1) (Qpositive_le_to_Qpositive_le' _ _ H2); clear H H1 H2. unfold Qpositive_le', Qpositive_sub in |- *; simpl in |- *; rewrite Heq; rewrite Heq'; rewrite Heq''. intros Hle Hle1 Hle2. 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:(p3) ipattern:(q3) ipattern:(Heq3) ipattern:(Heq1) ipattern:(Heq2). 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:(p4) ipattern:(q4) ipattern:(Heq4) ipattern:(Heq5) ipattern:(Heq6). apply Nat.mul_le_mono_pos_l with (S d'); auto with arith. repeat rewrite (Nat.mul_comm (S d')); rewrite (Nat.mul_comm (S p4)); repeat rewrite <- Nat.mul_assoc. rewrite <- Heq5; rewrite <- Heq6. 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 <- Heq1; rewrite <- Heq2. rewrite Nat.mul_comm. rewrite <- Nat.mul_assoc. repeat rewrite Nat.mul_sub_distr_r. repeat rewrite (Nat.mul_comm (S q'')). repeat rewrite <- (Nat.mul_assoc (S p'')). rewrite (Nat.mul_assoc (S q')). rewrite (Nat.mul_assoc (S q)). rewrite (Nat.mul_comm (S q) (S q')). apply le_minus_left. rewrite <- (Nat.mul_assoc (S q')). rewrite (Nat.mul_assoc (S p'')). repeat rewrite <- (Nat.mul_comm (S q * S q'')). replace (S q * S q'') with (S (q'' + q * S q'')). apply (fun m n p : nat => Nat.mul_le_mono_l p n m). exact Hle1. auto. repeat rewrite <- (Nat.mul_comm (S q')) || rewrite Nat.mul_assoc. repeat rewrite <- Nat.mul_assoc; apply (fun m n p : nat => Nat.mul_le_mono_l p n m). repeat rewrite Nat.mul_assoc; repeat rewrite <- (Nat.mul_comm (S q'')); apply (fun m n p : nat => Nat.mul_le_mono_l p n m). rewrite (Nat.mul_comm (S q'')); exact Hle. repeat rewrite Nat.mul_assoc; repeat rewrite <- (Nat.mul_comm (S q'')); apply (fun m n p : nat => Nat.mul_le_mono_l p n m). repeat rewrite <- Nat.mul_assoc; apply (fun m n p : nat => Nat.mul_le_mono_l p n m). exact Hle2. case (le_gt_dec (S p'' * S q') (S p' * S q'')). intros l; try assumption. elim Hneq2. rewrite <- (construct_correct w' (S p') (S q') (S p' + S q')); auto with *. rewrite <- (construct_correct w'' (S p'') (S q'') (S p'' + S q'')); auto with *. apply construct_correct4'; auto with arith. CaseEq (S p'' * S q' - S p' * S q''). intros Dummy Dummy2; generalize (minus_O_le _ _ Dummy); intros Dummy1; apply Nat.le_ngt in Dummy1; contradict Dummy1; assumption. auto with arith. apply Nat.add_le_mono_r. eapply Nat.le_trans; [ eapply minus_le | auto with arith ]. case (le_gt_dec (S p'' * S q) (S p * S q'')). intros l; try assumption. elim Hneq1. rewrite <- (construct_correct w (S p) (S q) (S p + S q)); auto with *. rewrite <- (construct_correct w'' (S p'') (S q'') (S p'' + S q'')); auto with *. apply construct_correct4'; auto with arith. CaseEq (S p'' * S q - S p * S q''). intros Dummy Dummy2; generalize (minus_O_le _ _ Dummy); intros Dummy1; apply Nat.le_ngt in Dummy1; contradict Dummy1; assumption. auto with arith. apply Nat.add_le_mono_r. eapply Nat.le_trans; [ eapply minus_le | auto with arith ]. Qed.