proposition: Theorem Q_distr_left : forall x y z : Q, Qmult (Qplus x y) z = Qplus (Qmult x z) (Qmult y z).
proof: Proof. intros x y z; case z. repeat rewrite <- (Qmult_sym Zero); repeat rewrite Qmult_zero; auto with *. exact (Q_distr_left_aux x y). intros z'. rewrite <- (Qplus_zero_left (Qmult (Qplus x y) (Qneg z'))). rewrite <- (Q_opp_def (Qplus (Qmult x (Qneg z')) (Qmult y (Qneg z')))). rewrite Qopp_plus. repeat rewrite Qmult_neg. rewrite <- Q_distr_left_aux. rewrite <- (Qmult_neg (Qplus x y)). repeat rewrite <- Qplus_assoc. rewrite <- (Qplus_sym (Qmult (Qplus x y) (Qneg z'))). rewrite Q_opp_def. rewrite <- (Qplus_sym Zero). rewrite Qplus_zero_left. auto. Qed.