proposition: Lemma FK_correct : Kchain_correct n 1 (FK cn).
proof: Proof. intros A op one equ M x s; specialize (Hn _ _ _ _ M x (x::s)). inversion Hn; subst; cbn. rewrite Hn; right; split; 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)