proposition: Lemma correct_app : Fchain_correct (n * p) (cn ++ cp).
proof: Proof. intros A op one equ M x s. rewrite exec_app. specialize (Hn _ _ _ _ M x s); inversion Hn; subst. specialize (Hp _ _ _ _ M x0 s0); inversion Hp; subst. right; destruct H3. split. - rewrite H2; destruct H1. cbn in *;rewrite H1, Pos_bpow_of_bpow; now rewrite Pos.mul_comm. - transitivity s0;auto. inversion H1;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)