proposition: Lemma lnot_nonneg : forall a, 0 <= lnot a <-> a < 0.
proof: Proof. intros a; unfold lnot. now rewrite <- opp_succ, opp_nonneg_nonpos, le_succ_l. Qed.
imports: Bool ZAxioms ZMulOrder ZPow ZDivFloor ZSgnAbs ZParity NZLog