proposition: Theorem Q_distr_left_aux : forall (x y : Q) (z' : Qpositive), Qmult (Qplus x y) (Qpos z') = Qplus (Qmult x (Qpos z')) (Qmult y (Qpos z')).
proof: Proof. intros x y z'; case y. repeat rewrite <- (Qplus_sym Zero). repeat rewrite Qplus_zero_left; auto with *. case x. simpl in |- *; auto with *. intros x' y'; simpl in |- *. rewrite Qpositive_mult_distr. auto. intros x' y'; simpl in |- *. Case' (Qpositive_le_dec x' y'). case (Qpositive_eq_dec x' y'). simpl in |- *. intros Heq; rewrite Heq. Case' (Qpositive_le_dec (Qpositive_mult y' z') (Qpositive_mult y' z')). case (Qpositive_eq_dec (Qpositive_mult y' z') (Qpositive_mult y' z')). auto. intros H; elim H; auto. intros H; elim H; auto. Case' (Qpositive_le_dec (Qpositive_mult x' z') (Qpositive_mult y' z')). case (Qpositive_eq_dec (Qpositive_mult x' z') (Qpositive_mult y' z')). intros e q n q0; elim n. apply Qpositive_mult_simpl with z'. auto. simpl in |- *; intros; rewrite Qpositive_mult_minus_distr; auto with *. intros H H0 H1 n q; elim H. apply Qpositive_le_antisym; auto. apply Qpositive_le_mult; auto with *. Case' (Qpositive_le_dec (Qpositive_mult x' z') (Qpositive_mult y' z')). case (Qpositive_eq_dec (Qpositive_mult x' z') (Qpositive_mult y' z')). intros e q H H0 H1; elim H. apply Qpositive_mult_simpl with z'; auto. intros n q H H0 H1; elim H. apply Qpositive_mult_simpl with z'; apply Qpositive_le_antisym; auto with *. apply Qpositive_le_mult; auto. intros H H0 H3 H1 H2 H4. simpl in |- *. rewrite Qpositive_mult_minus_distr; auto. intros y'; case x. simpl in |- *; repeat rewrite Qplus_zero_left; auto. intros x'; simpl in |- *. Case' (Qpositive_le_dec x' y'). case (Qpositive_eq_dec x' y'). Case' (Qpositive_le_dec (Qpositive_mult x' z') (Qpositive_mult y' z')). case (Qpositive_eq_dec (Qpositive_mult x' z') (Qpositive_mult y' z')). auto. intros n q e q0; elim n; rewrite e; auto. intros n H0 H1 e q; elim n; rewrite e; auto. Case' (Qpositive_le_dec (Qpositive_mult x' z') (Qpositive_mult y' z')). case (Qpositive_eq_dec (Qpositive_mult x' z') (Qpositive_mult y' z')). intros e q n; elim n; apply Qpositive_mult_simpl with z'; auto. simpl in |- *. intros; rewrite Qpositive_mult_minus_distr; auto with *. intros H H0 H1 n q; elim H1; apply Qpositive_le_mult; auto with *. Case' (Qpositive_le_dec (Qpositive_mult x' z') (Qpositive_mult y' z')). case (Qpositive_eq_dec (Qpositive_mult x' z') (Qpositive_mult y' z')). intros e q n; elim n; apply Qpositive_mult_simpl with z'; auto. intros n q H H0 H1; elim n. apply Qpositive_le_antisym; auto. apply Qpositive_le_mult; auto with *. simpl in |- *. intros; rewrite Qpositive_mult_minus_distr; auto. intros x'; simpl in |- *; rewrite Qpositive_mult_distr; auto with *. Qed.