proposition: Lemma inj_min p q : Z.pos (Pos.min p q) = Z.min (Z.pos p) (Z.pos q).
proof: Proof. unfold Z.min, Pos.min. rewrite inj_compare. now case Z.compare_spec. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass