proposition: Lemma graph_relation_spec {k : nat} (G : graph k) : forall x y, graph_relation G x y <-> (forall f : fin k, match G f with | Some (weight, d) => if weight then k_tuple_val f x < k_tuple_val d y else Peano.le (k_tuple_val f x) (k_tuple_val d y) | None => False end).
proof: Proof. unfold graph_relation. intros x y. now rewrite k_related_spec. Qed.
imports: Equations(Equations) Examples.Fin Relations Utf8 Relations Wellfounded Setoid RelationClasses Morphisms Lia Bool List Arith String Coq(FunctionalExtensionality) ssreflect