proposition: Lemma PO8 :forall (s : signature) (p d : positive), s = gen_K p d -> forall anonymous : p <> 1, pos_eq_dec p 1 = right anonymous -> forall (q r : N) (p0 : positive), r = N.pos p0 -> N.pos_div_eucl (p + d) (N.pos p) = (q, N.pos p0) -> (signature_measure (gen_F (N2pos q)) < signature_measure (gen_K p d))%nat.
proof: Proof. intros; unfold signature_measure. assert (N2pos q < p+d)%positive. quotient_small H2 H5. generalize anonymous; destruct p; simpl; try reflexivity. now destruct 1. generalize (pos_div_eucl_quotient_pos _ _ _ _ H2). intros H6; destruct q;auto. destruct H6;auto with chains. rewrite pos2N_inj_add; apply N.le_add_r;auto with chains. + revert H3; pos2nat_inj_tac; intros;lia. Qed.
imports: Coq(Inverse_Image Inclusion Wf_nat NArith Arith PArith Recdef Wf_nat Lexicographic_Product Lia) additions(Addition_Chains Compatibility More_on_positive Wf_transparent Dichotomy BinaryStrat) Coq(Lia)