proposition: Lemma rem_lt : forall a b r : positive, (Zpos a mod Zpos b)%Z = Zpos r -> pp_lt (b, r) (a, b).
proof: Proof. intros a b r Hr. generalize (Z_mod_lt (Zpos a) (Zpos b)). intro H; elim H; clear H. intros H0 H1. rewrite Hr in H1. unfold pp_lt in |- *. auto with zarith. auto with zarith. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)