proposition: Lemma PO9 :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_K (N2pos (N.pos p0)) (p - N2pos (N.pos p0))) < signature_measure (gen_K p d))%nat.
proof: Proof. intros; unfold signature_measure. apply Nat.add_lt_mono_r. rewrite <- (Nat.mul_lt_mono_pos_l (S _)); [| auto with arith]. rewrite Pplus_minus. + apply Pos2Nat.inj_lt; apply Pos.lt_add_diag_r; cbn. + generalize (N.pos_div_eucl_remainder (p + d) (N.pos p) ); rewrite H2; cbn; unfold N.lt ; intro H5; red. simpl in H5; now rewrite Pos.compare_antisym, H5. 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)