proposition: Lemma inj_max x y : Z.to_pos (Z.max x y) = Pos.max (Z.to_pos x) (Z.to_pos y).
proof: Proof. destruct x; simpl; try rewrite Pos.max_1_l. - now destruct y. - destruct y; simpl; now rewrite ?Pos.max_1_r, <- ?Pos2Z.inj_max. - destruct y; simpl; rewrite ?Pos.max_1_r; trivial. apply to_pos_nonpos. now apply Z.max_lub. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass