fact: Fixpoint Fexp2_of_nat (n:nat) : Fchain := match n with O => F1 | S p => Fcompose F2 (Fexp2_of_nat p) end.
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)