proposition: Lemma Zmod_POS_nonNEG : forall a b p : positive, (Zpos a mod Zpos b)%Z <> Zneg p.
proof: Proof. intros a b p. generalize (Z_mod_lt (Zpos a) (Zpos b)). intro H. elim H. intros H0 H1. intro Hfalse. rewrite Hfalse in H0. elim H0. auto with zarith. auto with zarith. Qed.
imports: CoRN.model.Zmod.ZBasics