proposition: Lemma KFF_correct: Fchain_correct (p * q + r) (KFF kpr mq).
proof: Proof. red; unfold KFF; intros; cbn. generalize (Eop_proper M); intros Hprop. rewrite exec_app. specialize (Hpr _ _ _ _ M x s). inversion Hpr; subst. inversion H1;subst; cbn in *. inversion H2;subst; rewrite exec_app. specialize (Hq _ _ _ _ M x0 (x1::s1)). inversion Hq;subst. inversion H5; cbn in H4, H8; cbn. inversion H8; subst; right; split. - cbn; fold mult_op; rewrite Pos_bpow_of_plus, H4, H0, Pos.mul_comm, Pos_bpow_of_bpow, H12, H6; reflexivity. - cbn; now transitivity s1. 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)