proposition: Lemma neg_lt_neg p q : (q < p)%positive -> Zneg p < Zneg q.
proof: Proof. intros; unfold Z.lt; simpl. now rewrite <- Pos.compare_antisym. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass