proposition: Lemma inj_min x y : Z.to_pos (Z.min x y) = Pos.min (Z.to_pos x) (Z.to_pos y).
proof: Proof. destruct x; simpl; try rewrite Pos.min_1_l. - now destruct y. - destruct y; simpl; now rewrite ?Pos.min_1_r, <- ?Pos2Z.inj_min. - destruct y; simpl; rewrite ?Pos.min_1_r; trivial. apply to_pos_nonpos. apply Z.min_le_iff. now left. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass