proposition: Lemma FFK_correct : Kchain_correct (p * q) p (FFK cp cq).
proof: Proof. red; intros; unfold FFK; cbn; rewrite exec_app. specialize (Hp A op one equ M x s); inversion Hp; subst; cbn. inversion H1; subst. specialize (Hq A op one equ M x0 (x0::s0));inversion Hq; subst. rewrite H3, Hq; right; inversion H5; split. - cbn in *; rewrite H0; repeat rewrite Pos_bpow_ok; rewrite power_of_power. apply power_proper; auto. + reflexivity. + rewrite Pos2Nat.inj_mul; now rewrite Nat.mul_comm. - transitivity s1;auto. + inversion H5;auto. now symmetry. + transitivity (x0::s0); auto. 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)