proposition: Lemma Zabs_10 : forall z : Z, (0 <= Z.abs z)%Z.
proof: Proof. intro. case (Z_zerop z). intro. rewrite e. simpl in |- *. apply Z.le_refl. intro. case (not_Zeq z 0 n). intro. apply Zlt_le_weak. apply Zabs_9. apply Z.le_refl. simpl in |- *. right. assumption. intro. apply Zlt_le_weak. apply Zabs_9. apply Z.le_refl. simpl in |- *. left. assumption. Qed.
imports: Coq(Lia)