proposition: Lemma Zabs_lt_pos : forall a b : Z, (Z.abs a < b)%Z -> (0 < b)%Z.
proof: Proof. intros a b Hab. unfold Z.lt in |- *. elim (Zcompare_Gt_Lt_antisym b 0). intros H1 H2. apply H1. fold (b > 0)%Z in |- *. apply (Zgt_le_trans b (Z.abs a) 0); auto with zarith. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq(Lia)