proposition: Lemma sct_power_check {k} G (T : relation (k_tuple_type k)) : approximates G T -> (exists n f, power_graph_n n G f = Some (true, f)) -> (forall x y, T x y -> TI _ y x -> False).
proof: Proof. intros approx [n [f eqpow]] x y Txy TIyx. assert (compose_rel T (TI k) x x). exists y; easy. assert (power n (compose_rel T (TI k)) x x). { clear -H. induction n; simp power; auto. exists x. intuition. } pose (compose_approximates G (TI_graph k) T (TI k)). forward a; auto. forward a; auto. unfold TI. red. intuition. rewrite TI_compose' in a. apply (approximates_power n) in a. specialize (a x x). specialize (a H0). rewrite -> graph_relation_spec in a. specialize (a f). rewrite eqpow in a. lia. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect