proposition: Lemma inj_succ p : Z.pos (Pos.succ p) = Z.succ (Z.pos p).
proof: Proof. simpl. now rewrite Pos.add_1_r. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass