proposition: Lemma fcompose_assoc A B C D (f: C -> D) (g : B -> C) (h : A -> B) : fcompose (fcompose f g) h = fcompose f (fcompose g h).
proof: Proof. done. Qed.
imports: Arith micromega.Lia Setoid IndefiniteDescription ClassicalChoice HahnBase HahnList HahnEquational HahnRewrite HahnRelationsBasic HahnSets HahnNatExtra HahnListBefore HahnWf HahnSorted HahnTotalExt