proposition: Lemma Z_abs_triangle : forall x y, Z.abs (x + y) <= Z.abs x + Z.abs y.
proof: Proof. Proof Z.abs_triangle. Lemma Z_add_opp_diag_r : forall x, x + -x = 0. Proof Z.add_opp_diag_r. #[local] Instance Z_opp_ge_le_compat : Proper (Z.ge ==> Z.le) Z.opp. Proof. intros x y. lia. Qed.
imports: AAC_tactics(AAC)