proposition: Theorem Q_opp_def : forall n : Q, Qplus n (Qopp n) = Zero.
proof: Proof. intros n; case n; simpl in |- *; auto. intros n'; Case' (Qpositive_le_dec n' n'). case (Qpositive_eq_dec n' n'); auto. intros H; elim H; auto. intros H; elim H; auto. intros n'; Case' (Qpositive_le_dec n' n'). case (Qpositive_eq_dec n' n'); auto. intros H; elim H; auto. intros H; elim H; auto. Qed.