proposition: Lemma inj_neg_iff p q : Z.neg p = Z.neg q <-> p = q.
proof: Proof. split. - apply inj_neg. - intros; now f_equal. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass