proposition: Lemma divide_Zpos_Zneg_r n p : (n|pos p) <-> (n|neg p).
proof: Proof. split; intros (m,H); exists (-m); now rewrite mul_opp_l, <- H. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass