proposition: Lemma Fexp2_nat_correct (n:nat) : Fchain_correct_nat (2 ^ n) (Fexp2_of_nat n).
proof: Proof. induction n; cbn. - apply F1_correct. - rewrite Nat.add_0_r; replace (2 ^ n + 2 ^ n)%nat with (2 * 2 ^n)%nat by lia; apply Fcompose_correct_nat;auto. + apply F2_correct. + apply Fexp2_nat_proper. 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)