proposition: Lemma inj_pred p : p <> 1%positive -> Z.pos (Pos.pred p) = Z.pred (Z.pos p).
proof: Proof. destruct p; easy || now destruct 1. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass