proposition: Theorem Qpositive_mult_minus_distr : forall w w' w'' : Qpositive, w <> w' -> Qpositive_le w w' -> Qpositive_mult (Qpositive_sub w' w) w'' = Qpositive_sub (Qpositive_mult w' w'') (Qpositive_mult w w'').
proof: Proof. intros w w' w'' Hneq. cut (Qpositive_mult w w'' <> Qpositive_mult 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 H; generalize (Qpositive_le_mult _ _ w'' H); intros H1; generalize (Qpositive_le_to_Qpositive_le' _ _ H1) Hneq1; generalize (Qpositive_le_to_Qpositive_le' _ _ H); clear H H1 Hneq1. unfold Qpositive_le', Qpositive_mult, Qpositive_sub in |- *; rewrite Heq; 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:(p3) ipattern:(q3) ipattern:(Heq1) ipattern:(Heq2) ipattern:(Heq3). 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). expand (S p * S p'') (S q * S q'') (S p * S p'' + S q * S q'') ipattern:(d'') ipattern:(p5) ipattern:(q5) ipattern:(Heq7) ipattern:(Heq8) ipattern:(Heq9). intros Hle1. intros Hneq1. apply construct_correct4'; try (simpl in |- *; auto with arith; fail). case (le_gt_dec (S p4 * S q5) (S p5 * S q4)). intros l. elim Hneq1. apply construct_correct4'; try (simpl in |- *; auto with arith; fail). rewrite Heq8; rewrite Heq9; rewrite Heq5; rewrite Heq6. replace (S p5 * S d'' * (S q4 * S d')) with (S p5 * S q4 * (S d'' * S d')). replace (S p4 * S d' * (S q5 * S d'')) with (S p4 * S q5 * (S d'' * S d')). apply f_equal with (f := fun x : nat => x * (S d'' * S d')). apply Nat.le_antisymm; auto. ring. ring. CaseEq (S p4 * S q5 - S p5 * S q4). 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 Nat.le_sub_l | auto with arith ]. apply mult_reg_l with d. rewrite <- (Nat.mul_assoc (S p3)); rewrite (Nat.mul_assoc (S d)); rewrite <- (Nat.mul_comm (S p3)); rewrite <- Heq2. rewrite (Nat.mul_comm (S q3)); rewrite (Nat.mul_comm (S d)); repeat rewrite <- Nat.mul_assoc. rewrite <- Heq3. apply mult_reg_l with d'. rewrite (Nat.mul_comm (S q4)). rewrite (Nat.mul_comm (S d')); repeat rewrite <- Nat.mul_assoc. rewrite <- Heq6. rewrite Nat.mul_sub_distr_r; repeat rewrite (Nat.mul_comm (S p4)) || rewrite (Nat.mul_comm (S q4)) || rewrite <- Nat.mul_assoc; try (rewrite (Nat.mul_comm (S d')); rewrite Nat.mul_sub_distr_r; repeat rewrite <- Nat.mul_assoc; rewrite <- Heq5; rewrite <- Heq6). rewrite (Nat.mul_comm (S d')); repeat rewrite Nat.mul_sub_distr_r; repeat rewrite (Nat.mul_comm (S p4)) || rewrite (Nat.mul_comm (S q4)) || rewrite <- Nat.mul_assoc. repeat rewrite (Nat.mul_comm (S d')); rewrite <- Heq5; rewrite <- Heq6. apply mult_reg_l with d''. repeat rewrite (Nat.mul_comm (S p5)) || rewrite (Nat.mul_comm (S q5)) || rewrite <- Nat.mul_assoc. repeat rewrite (Nat.mul_comm (S d'')); repeat rewrite Nat.mul_sub_distr_r; repeat rewrite <- Nat.mul_assoc; rewrite <- Heq8; rewrite <- Heq9. apply minus_decompose; ring. case (le_gt_dec (S p' * S q) (S p * S q')); [ intros l; elim Hneq | idtac ]. rewrite <- construct_correct with (1 := Heq) (n := S p + S q); try (simpl in |- *; auto with arith; fail). rewrite <- construct_correct with (1 := Heq') (n := S p' + S q'); try (simpl in |- *; auto with arith; fail). apply construct_correct4'; try (simpl in |- *; auto with arith; fail). 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 Nat.le_sub_l | auto with arith ]. red in |- *; intros H; elim Hneq; rewrite <- (Qpositive_mult_One w); rewrite <- (Qpositive_mult_One w'). repeat rewrite (Qpositive_mult_sym One). rewrite <- (Qpositive_mult_inv w''); repeat rewrite <- Qpositive_mult_assoc; rewrite H; auto. Qed.