proposition: Lemma Fexp2_correct (p:positive) : Fchain_correct (2 ^ p) (Fexp2 p).
proof: Proof. intros;red. rewrite Pos_pow_power, Pos2Nat_morph. generalize (Fexp2_nat_correct (Pos.to_nat p)). unfold Fexp2. change (Pos.to_nat 2) with 2%nat. replace (2 ^ Pos.to_nat p)%nat with (2%nat ^ Pos.to_nat p)%M. auto. now rewrite nat_power_ok. 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)