proposition: Lemma Zabs_triangle : forall a b : Z, (Z.abs (a + b) <= Z.abs a + Z.abs b)%Z.
proof: Proof. intros a b. case a; case b. 1-5, 7, 9: auto with zarith. intros p q. generalize (case_POS p q) (case_NEG p q). case (Zpos q + Zneg p)%Z. auto with zarith. intros p0 case_POS0 case_NEG0. apply (case_POS0 p0). reflexivity. intros p0 case_POS0 case_NEG0. apply (case_NEG0 p0). reflexivity. intros p q. rewrite (Zplus_comm (Zneg q) (Zpos p)). rewrite (Zplus_comm (Z.abs (Zneg q)) (Z.abs (Zpos p))). generalize (case_POS q p) (case_NEG q p). case (Zpos p + Zneg q)%Z. auto with zarith. intros p0 case_POS0 case_NEG0. apply (case_POS0 p0). reflexivity. intros p0 case_POS0 case_NEG0. apply (case_NEG0 p0). reflexivity. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq(Lia)