proposition: Lemma rem_dec : forall a b : positive, ((Zpos a mod Zpos b)%Z = 0%Z) or ({r : positive| (Zpos a mod Zpos b)%Z = Zpos r}).
proof: Proof. intros a b. set (r := (Zpos a mod Zpos b)%Z) in *. assert (Hr : r = (Zpos a mod Zpos b)%Z); auto; generalize Hr. case (Zpos a mod Zpos b)%Z. intros; left; auto. intros p Hp; right; exists p; auto. intros p Hp; unfold r in Hp; elim (Zmod_POS_nonNEG _ _ _ Hp). Defined.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)