proposition: Lemma Qcabs_triangle : forall x y : Qc, Qcabs (x+y) <= Qcabs x + Qcabs y.
proof: Proof. intros x y. unfold Qcle,Qcplus. do 3 apply Qcabs_case; intros Hy Hx Hxy. - apply Zmult_le_compat_r;auto with *. - apply Qcplus_le_compat; apply Qcle_refl || (abstract (transitivity 0; easy || now rewrite Qcle_minus_iff in Hy,Hx; rewrite Qcplus_0_l in *)). - apply Qcplus_le_compat; apply Qcle_refl || (abstract (transitivity 0; easy || now rewrite Qcle_minus_iff in Hy,Hx; rewrite Qcplus_0_l in *)). - apply Qcplus_le_compat; apply Qcle_refl || (abstract (transitivity 0; easy || now rewrite Qcle_minus_iff in Hy,Hx; rewrite Qcplus_0_l in *)). - change (- (x + y) <= x + y). transitivity 0. rewrite Qcle_minus_iff. rewrite Qcopp_involutive. rewrite Qcplus_0_l. rewrite <- Qcplus_0_r at 1. now apply Qcplus_le_compat. rewrite <- Qcplus_0_r at 1. now apply Qcplus_le_compat. - change (- (x + y) <= x + (- y)). rewrite Qcopp_distr_plus. apply Qcplus_le_compat. transitivity 0. change 0 with (-0). now apply Qcopp_le_compat. easy. reflexivity. - change (- (x + y) <= (- x) + y). rewrite Qcopp_distr_plus. apply Qcplus_le_compat. reflexivity. transitivity 0. change 0 with (-0). now apply Qcopp_le_compat. easy. - change (- (x + y) <= (- x) + (- y)). rewrite Qcopp_distr_plus. reflexivity. Qed.
imports: Qreduction ClassicalRealizability.Qccomplement