proposition: Lemma approximates_power {k} (n : nat) (g : graph k) T : approximates g T -> approximates (power_graph_n n g) (power n T).
proof: Proof. induction n; simp power power_graph_n; auto. intros. specialize (IHn H). now apply compose_approximates. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect