proposition: Lemma fexpS A (f : A -> A) n x : fexp f n (f x) = f (fexp f n x).
proof: Proof. by revert x; induction n; ins; unfold fcompose; rewrite IHn. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt