proposition: Lemma Zabs_neg : forall z : Z, (z <= 0)%Z -> Z.abs z = (- z)%Z.
proof: Proof. intro. case z. simpl in |- *. intro. reflexivity. intros. apply False_ind. apply H. simpl in |- *. reflexivity. intros. simpl in |- *. reflexivity. Qed.
imports: Coq(Lia)