proposition: Lemma divide_Zpos p q : (pos p|pos q) <-> (p|q)%positive.
proof: Proof. split. - intros ([ |r|r],H); simpl in *; destr_eq H. exists r; auto. - intros (r,H). exists (pos r); simpl; now f_equal. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass