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