proposition: Lemma L0: Fchain_correct n c.
proof: Proof. assert (H: OK (gen_F n) c) by apply chain_gen_OK. red; intros; destruct (H A op one equ M x s). - left. - now right. 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)