proposition: Lemma PO6: 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, r = 0%N -> N.pos_div_eucl (p + d) (N.pos p) = (q, 0%N) -> (signature_measure (gen_F (N2pos q)) < signature_measure (gen_K p d))%nat.
proof: Proof. intros; unfold signature_measure. quotient_small H2 H5. destruct p; (discriminate || reflexivity). N2pos_destruct q q. + destruct (pos_div_eucl_quotient_pos _ _ _ _ H2);auto with chains. rewrite pos2N_inj_add; apply N.le_add_r. + simpl; rewrite <- pos2N_inj_lt in H5; rewrite Pos2Nat.inj_lt in H5. 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)