proposition: Lemma F3_correct : Fchain_correct 3 F3.
proof: Proof. constructor; intros. cbn. fold mult_op. constructor. - cbn; now rewrite Eop_assoc. - apply Stack_equiv_refl. 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)