proposition: Lemma F2q_correct (n:positive) : Fchain_correct (2 ^ n) (F2q n).
proof: Proof. unfold F2q. replace (2 ^n)%positive with (Pos.of_nat (2 ^ Pos.to_nat n)%nat). apply F2q_correct_1. rewrite Compatibility.Pos_pow_power. rewrite <- Pos_bpow_ok_R. - rewrite Pos_bpow_ok. + rewrite Nat2Pos.id. * generalize (Pos.to_nat n). intros; rewrite Compatibility.nat_power_ok. induction n0; simpl; auto. rewrite Nat2Pos.inj_mul. -- rewrite IHn0; simpl (Pos.of_nat 2). f_equal. unfold mult_op; unfold P_mult_op. f_equal. -- discriminate. -- clear IHn0; induction n0;simpl. ++ discriminate. ++ remember (2%nat ^ n0) as n1. unfold mult_op. unfold nat_mult_op. lia. * apply Pos_to_nat_diff_0. - apply Pos_to_nat_diff_0. Qed.
imports: Coq(List PArith Relations Lia) additions(Monoid_def Monoid_instances Strategies) Coq(Recdef Wf_nat) additions(More_on_positive Pow Euclidean_Chains Dichotomy BinaryStrat) Coq(NArith)