proposition: Lemma Qabs_triangle: forall p q, Qabs (p + q) <= Qabs p + Qabs q.
proof: Proof. intros p q. destruct (Q_le_lt_dec Zero p) as [Hp|Hp]; destruct (Q_le_lt_dec Zero q) as [Hq|Hq]. repeat rewrite Qabs_eq; auto. assert (Hp1:=Qabs_eq _ Hp); assert (Hq1:=Qabs_non_eq_neg _ Hq); rewrite Hp1; rewrite Hq1; destruct (Q_le_lt_dec Zero (p+q)) as [Hpq|Hpq]. rewrite Qabs_eq; trivial; apply Qle_Zero_Qminus_neg; stepl (q+q);[|ring]; auto. rewrite Qabs_non_eq_neg; trivial; apply Qle_Zero_Qminus; stepr (p+p);[|ring]; auto. assert (Hp1:=Qabs_non_eq_neg _ Hp); assert (Hq1:=Qabs_eq _ Hq); rewrite Hp1; rewrite Hq1; destruct (Q_le_lt_dec Zero (p+q)) as [Hpq|Hpq]. rewrite Qabs_eq; trivial; apply Qle_Zero_Qminus_neg; stepl (p+p);[|ring]; auto. rewrite Qabs_non_eq_neg; trivial; apply Qle_Zero_Qminus; stepr (q+q);[|ring]; auto. repeat rewrite Qabs_non_eq_neg; auto; (stepr (-(p+q)) by ring); trivial. Qed.