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