proposition: Lemma PO3 : 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_F (N2pos q)) < signature_measure (gen_F i))%nat.
proof: Proof. intros; unfold signature_measure. gamma_bounds gamma i H12 H14. quotient_small H4 H5. rewrite <- Nat.mul_lt_mono_pos_l ; [ | auto with arith chains]. apply Pos2Nat.inj_lt. destruct q; simpl in *. transitivity (gamma i);auto. now rewrite pos2N_inj_lt. 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)