proposition: Lemma PO4 : forall (s : signature) (i : positive), s = gen_F i -> forall anonymous : i <> 1, pos_eq_dec i 1 = right anonymous -> forall anonymous0 : i <> 3, pos_eq_dec i 3 = right anonymous0 -> exact_log2 i = None -> forall (q r : N) (p : positive), r = N.pos p -> N.pos_div_eucl i (N.pos (gamma i)) = (q, N.pos p) -> (signature_measure (gen_K (N2pos (N.pos p)) (gamma i - N2pos (N.pos p))) < signature_measure (gen_F i))%nat.
proof: Proof. intros; unfold signature_measure. apply lt_S_2i; rewrite Pplus_minus. gamma_bounds gamma i H5 H6. + apply Pos2Nat.inj_lt; auto. + rest_small H4 H5; now apply Pos.lt_gt. 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)