proposition: Lemma F2q_correct_1 (n:nat) : Fchain_correct (Pos.of_nat (2 ^ n)) (F2q_of_nat n).
proof: Proof. red;intros; intros; rewrite F2q_correct_0. right; split. - cbn;rewrite Pos_bpow_ok_R. + reflexivity. + apply Nat.pow_nonzero. discriminate. - reflexivity. 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)