proposition: Lemma F2q_correct_0: forall `{M : @EMonoid A op one equ} (n:nat) x s, result_equiv (exec A op (F2q_of_nat n) x s) (Some(Pow.power x (2 ^ n), s)).
proof: Proof. induction n. - simpl. intros; f_equal; right; split. + cbn; rewrite Eone_right. reflexivity. + reflexivity. - intro x; simpl; intro s; rewrite IHn. right; split;auto. + cbn. replace (2 ^ n + (2 ^ n + 0))%nat with (2 * ( 2 ^ n) )%nat. * fold mult_op; assert (x * x == x ^2) by (now rewrite sqr_eqn). transitivity ((x ^ 2) ^2 ^ n). now apply power_proper. rewrite power_of_power. apply power_proper. reflexivity. lia. * lia. + 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)