proposition: Lemma PO1 :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, r = 0%N -> N.pos_div_eucl i (N.pos (gamma i)) = (q, 0%N) -> (signature_measure (gen_F (N2pos q)) < signature_measure (gen_F i))%nat.
proof: Proof. intros; unfold signature_measure. generalize (N.pos_div_eucl_spec i (N.pos (gamma i))). rewrite H4; N2pos_destruct q p. subst r; repeat rewrite N.add_0_r. injection 1. intro H5 ;rewrite H5. gamma_bounds gamma i H12 H14. assert (H13 : p <> 1). + intro Hp ; subst p. simpl in H5. destruct (Pos.lt_irrefl i). now rewrite H5 at 1. + assert (H11 := pos_lt_mul p (gamma i) H12). rewrite Pos2Nat.inj_lt in H11. rewrite Pos2Nat.inj_mul in *; 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)