proposition: Lemma F2_correct : Fchain_correct 2 F2.
proof: Proof. intros until M; intros k Hk a; simpl; apply Hk; monoid_simpl M; reflexivity. 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)