proposition: Lemma PO2 : 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 (gamma i)) < signature_measure (gen_F i))%nat.
proof: Proof. intros; unfold signature_measure. rewrite <- Nat.mul_lt_mono_pos_l; [ apply Pos2Nat.inj_lt; apply gamma_lt|] ; auto with chains. 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)