proposition: Lemma pp_lt_wf : Wf.well_founded pp_lt.
proof: Proof. red in |- *. intros x. assert (forall (n : nat) (a b : positive), nat_of_P b < n -> Acc pp_lt (a, b)). simple induction n. intros a b H0. elim (Nat.nlt_0_r _ H0). intros n0 Hind a b HSn0. assert (Hdisj : nat_of_P b < n0 \/ nat_of_P b = n0). lia. elim Hdisj. apply Hind. intro Heq. assert (Hy : forall y : pp, pp_lt y (a, b) -> Acc pp_lt y). intro y; elim y; intros c d Hdb. unfold pp_lt in Hdb. assert (Hd : nat_of_P d < n0). rewrite <- Heq. apply nat_of_P_lt_Lt_compare_morphism. exact Hdb. apply Hind. exact Hd. exact (Acc_intro (a, b) Hy). elim x; intros a b. apply (H (S (nat_of_P b))). auto. Qed.
imports: CoRN.model.Zmod.ZDivides Coq.Init.Wf Coq(Lia)