proposition: Lemma KFK_correct : Kchain_correct (p * q + r) p (KFK kpr mq).
proof: Proof. red; unfold KFK. intros; cbn. generalize (Eop_proper M); intros Hprop. rewrite exec_app. specialize (Hpr _ _ _ _ M x s); inversion Hpr; subst; cbn. inversion H1;subst; cbn in *. destruct s0; [ inversion H2|]. inversion H2;subst; rewrite exec_app. specialize (Hq _ _ _ _ M x0 (a::x0::s0)). inversion Hq;subst. inversion H5. cbn in H4, H7. transitivity (Some (Pos_bpow x0 q * a, x0 :: s0)). - cbn; inversion H7; subst. right. split. * cbn; fold mult_op; cbn. rewrite H12, H4; reflexivity. * cbn; assumption. - right; split. + cbn; rewrite Pos_bpow_of_plus, H6. rewrite Pos.mul_comm, <- Pos_bpow_of_bpow, H0; reflexivity. + cbn; right; auto. 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)