proposition: Lemma Zabs_le_pos : forall a b : Z, (Z.abs a <= b)%Z -> (0 <= b)%Z.
proof: Proof. intros a b Hab. apply (Z.le_trans 0 (Z.abs a) b). auto with zarith. assumption. Qed.
imports: Coq.ZArith.ZArith CoRN.logic.CLogic Coq(Lia)