proposition: Theorem Qpositive_sub_correct2 : forall w w' : Qpositive, w <> w' -> Qpositive_le w' w -> Qpositive_plus (Qpositive_sub w w') w' = w.
proof: Proof. intros w w'; make_fraction w ipattern:(p) ipattern:(q) ipattern:(Heq); make_fraction w' ipattern:(p') ipattern:(q') ipattern:(Heq'). intros H H1; generalize (Qpositive_le_to_Qpositive_le' _ _ H1); clear H1. unfold Qpositive_le', Qpositive_plus, Qpositive_sub in |- *; rewrite Heq; rewrite Heq'. intros Hle. 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:(p2) ipattern:(q2) ipattern:(Heq1) ipattern:(Heq2) ipattern:(Heq3). rewrite <- (construct_correct _ _ _ (S p + S q) Heq). apply construct_correct4'; try (simpl in |- *; auto with arith; fail). apply mult_reg_l with d. rewrite Nat.mul_add_distr_r. rewrite <- (Nat.mul_assoc (S p2)); rewrite (Nat.mul_comm (S p2)); rewrite <- (Nat.mul_assoc (S p')); repeat rewrite (Nat.mul_comm (S q2)); repeat rewrite (Nat.mul_comm (S d)); rewrite Nat.mul_add_distr_r; repeat rewrite <- Nat.mul_assoc. rewrite <- Heq2; rewrite <- Heq3. rewrite (Nat.mul_assoc (S p) (S q')); rewrite (Nat.mul_assoc (S p') (S q)). rewrite (Nat.mul_assoc (S q') (S q)). rewrite (Nat.mul_comm (S q') (S q)); repeat rewrite (Nat.mul_comm (S q * S q')). rewrite <- Nat.mul_add_distr_r. apply f_equal with (f := fun x : nat => x * (S q * S q')). symmetry in |- *. rewrite Nat.sub_add; auto with arith. auto. apply Nat.le_succ_l. apply Nat.lt_eq_cases in Hle; destruct Hle as [|Heq1]. lia. elim H; rewrite <- construct_correct with (n := S p + S q) (1 := Heq); auto. rewrite <- construct_correct with (n := S p' + S q') (1 := Heq'); auto. apply construct_correct4'; auto with *. apply Nat.add_le_mono_r. eapply Nat.le_trans; [ eapply Nat.le_sub_l | apply Nat.le_add_r ]. Qed.