proposition: Lemma Zabs_Zminus_triangle : forall a b : Z, (Z.abs (Z.abs a - Z.abs b) <= Z.abs (a - b))%Z.
proof: Proof. assert (case : forall a b : Z, (Z.abs a - Z.abs b <= Z.abs (a - b))%Z). intros a b. unfold Z.le in |- *. unfold Zminus in |- *. rewrite <- (Zcompare_plus_compat (Z.abs a + - Z.abs b) (Z.abs (a + - b)) (Z.abs b)) . rewrite (Zplus_comm (Z.abs a) (- Z.abs b)). rewrite Zplus_assoc. rewrite (Zplus_comm (Z.abs b) (- Z.abs b)). rewrite Zplus_opp_l. rewrite Zplus_0_l. assert (l : forall a b : Z, a = (b + (a - b))%Z). auto with zarith. set (a' := a) in |- * at 2. rewrite (l a b). unfold a' in |- *. fold (a - b)%Z in |- *. apply (Zabs_triangle b (a - b)). intros a b. apply Zabs_le_elim. apply case. replace (- (Z.abs a - Z.abs b))%Z with (Z.abs b - Z.abs a)%Z by auto with zarith. rewrite Zabs_Zminus_symm. apply case. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq(Lia)